diff options
| -rwxr-xr-x | debian/rules | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index c9881e82..8e927795 100755 --- a/debian/rules +++ b/debian/rules @@ -58,7 +58,10 @@ install: build $(MAKE) $(ADDPREF) install || $(MAKE) BEST=byte HASCOQIDE=byte $(ADDPREF) install - for i in $(COQPREF)/usr/bin/*.opt; do strip -R .note -R .comment $$i; done + -for i in $(COQPREF)/usr/bin/*.opt; do \ + echo "Stripping: $$i"; \ + strip -R .note -R .comment $$i; \ + done cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm cp debian/coq.desktop debian/coqide/usr/share/applnk/Development |