diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 22:32:05 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 22:32:05 +0000 |
| commit | 39a05ea8ddf4411a5abd7ef804bd5d40ee8f3bda (patch) | |
| tree | 40bcde75f180ef968e8794a19f3d25982c63c942 /debian | |
| parent | 1aa163f8f8c548e69b94188497b72a5c1242edb1 (diff) | |
We only need to call check since world depends on it.
Diffstat (limited to 'debian')
| -rwxr-xr-x | debian/rules | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/debian/rules b/debian/rules index 62c14ed8..be9ce98e 100755 --- a/debian/rules +++ b/debian/rules @@ -25,29 +25,26 @@ configure-stamp: patch build: patch-stamp configure-stamp build-stamp build-stamp: dh_testdir + touch test-suite/success/debian.v8 if grep -q BEST=opt config/Makefile; \ then \ - echo opt > best-stamp; \ - $(MAKE) world \ + $(MAKE) check \ || (echo WARNING: NATIVE CODE COMPILATION FAILED \ && echo Trying to build coq in bytecode instead \ - && echo byte > best-stamp \ && $(MAKE) archclean clean \ - && $(MAKE) BEST=byte world \ + && touch test-suite/success/debian.v8 \ + && $(MAKE) BEST=byte check \ && echo NATIVE CODE COMPILATION FAILED \ && echo Coq was built in bytecode instead); \ else \ - echo byte > best-stamp; \ - $(MAKE) world; \ + $(MAKE) check; \ fi - touch test-suite/success/debian.v8 - $(MAKE) BEST=`cat best-stamp` check touch build-stamp clean: unpatch dh_testdir dh_testroot - rm -f build-stamp configure-stamp best-stamp + rm -f build-stamp configure-stamp -$(MAKE) clean -$(MAKE) archclean |