* Remove timing for -O0, people really shouldn't use it.

[ginac.git] / debian / ginac-dev.files

diff --git a/debian/ginac-dev.files b/debian/ginac-dev.files
index 898ea2e0e5a3afbd4fd55f5457fd6de093b81acb..066df4b0efdd844a8d05e6517117514ce2f90c42 100644 (file)
--- a/debian/ginac-dev.files
+++ b/debian/ginac-dev.files
@@ -4,3 +4,4 @@ usr/lib/libginac.so
 usr/include/ginac
 usr/bin/ginac-config
 usr/share/man/man1/ginac-config*
+usr/share/info