diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-16 20:35:05 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-16 20:35:05 +0000 |
commit | 0338182d89681992cd148ec1cea0d02f10c301d9 (patch) | |
tree | 8027281068cbefa18fe2fc8eb17f02c0d7cc210c /debian/rules | |
parent | 1d628357fa2c4ccf4c6a8d9e0d02c7f8de4f15fe (diff) |
Stupid mistake.
Diffstat (limited to 'debian/rules')
-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 |