diff options
Diffstat (limited to 'debian/rules')
| -rwxr-xr-x | debian/rules | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/debian/rules b/debian/rules index b9552a69..a2ae494e 100755 --- a/debian/rules +++ b/debian/rules @@ -63,13 +63,12 @@ install: build dh_installdirs $(MAKE) $(ADDPREF) install || $(MAKE) BEST=byte $(ADDPREF) install - -strip -R .note -R .comment $(COQPREF)/usr/bin/coqtop.opt - -strip -R .note -R .comment $(COQPREF)/usr/bin/coqide.opt - -strip -R .note -R .comment $(COQPREF)/usr/bin/coq-interface.opt -# -strip -R .note -R .comment $(COQPREF)/usr/bin/parser.opt + + for i in $(COQPREF); 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 - dh_install --sourcedir=$(COQPREF) + + dh_install --sourcedir=$(COQPREF) --fail-missing binary-indep: build install |