diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 16:28:26 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 16:28:26 +0000 |
| commit | c806af42e185257ef0f3e0646b3c95c8086ff715 (patch) | |
| tree | 475789d52e4345a10bf5562b2482bcf1f7fb1aa9 | |
| parent | 5d9fa80010162806e5157dfe8db58fe0b2b6d7bf (diff) | |
Check is now in byte when compiled in fallback byte.
| -rwxr-xr-x | debian/rules | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/debian/rules b/debian/rules index e4dc420a..23945313 100755 --- a/debian/rules +++ b/debian/rules @@ -27,27 +27,27 @@ build-stamp: dh_testdir if grep -q BEST=opt config/Makefile; \ then \ - export BEST=opt; \ + echo opt > best-stamp; \ $(MAKE) world \ || (echo WARNING: NATIVE CODE COMPILATION FAILED \ && echo Trying to build coq in bytecode instead \ - && export BEST=byte \ + && echo byte > best-stamp \ && $(MAKE) archclean clean \ && $(MAKE) BEST=byte world \ && echo NATIVE CODE COMPILATION FAILED \ && echo Coq was built in bytecode instead); \ else \ - export BEST=byte; \ + echo byte > best-stamp; \ $(MAKE) world; \ - fi; \ - touch test-suite/success/debian.v8; \ - $(MAKE) BEST=$$BEST check + fi + touch test-suite/success/debian.v8 + $(MAKE) BEST=$(shell cat best-stamp) check touch build-stamp clean: unpatch dh_testdir dh_testroot - rm -f build-stamp configure-stamp + rm -f build-stamp configure-stamp best-stamp -$(MAKE) clean -$(MAKE) archclean |