diff options
| -rwxr-xr-x | debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index a2ae494e..c13d36a4 100755 --- a/debian/rules +++ b/debian/rules @@ -64,7 +64,7 @@ install: build $(MAKE) $(ADDPREF) install || $(MAKE) BEST=byte $(ADDPREF) install - for i in $(COQPREF); do strip -R .note -R .comment $$i; done + for i in $(COQPREF)/usr/bin/*.opt; do strip -R .note -R .comment $$i; done install debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm install debian/coq.desktop debian/coqide/usr/share/applnk/Development |