summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-16 20:35:05 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-16 20:35:05 +0000
commit0338182d89681992cd148ec1cea0d02f10c301d9 (patch)
tree8027281068cbefa18fe2fc8eb17f02c0d7cc210c
parent1d628357fa2c4ccf4c6a8d9e0d02c7f8de4f15fe (diff)
Stupid mistake.
-rwxr-xr-xdebian/rules2
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