diff options
Diffstat (limited to 'debian/rules')
-rwxr-xr-x | debian/rules | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/debian/rules b/debian/rules index 44dac55d..a9bd3b67 100755 --- a/debian/rules +++ b/debian/rules @@ -57,7 +57,7 @@ build-stamp: patch-stamp configure-stamp clean: unpatch dh_testdir dh_testroot - rm -f build-stamp configure-stamp opt-stamp + rm -f build-stamp configure-stamp opt-stamp install-stamp [ ! -f config/Makefile ] || $(MAKE) clean [ ! -f config/Makefile ] || $(MAKE) archclean @@ -72,7 +72,8 @@ clean: unpatch dh_clean -install: build +install: install-stamp +install-stamp: build-stamp dh_testdir dh_testroot dh_clean -k @@ -115,6 +116,7 @@ install: build rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ dh_install --sourcedir=$(COQPREF) --list-missing + touch install-stamp binary-common: dh_testdir |