summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 13:53:34 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 13:53:34 +0000
commit5d9fa80010162806e5157dfe8db58fe0b2b6d7bf (patch)
treed4a3fe6718cc9550f92fb3d4ed49ff64bb7f1e7d
parent2f100c8cddd5b81aa26fc5db565e28b8e6c12713 (diff)
Opt with fallback on byte should work now.
-rwxr-xr-xdebian/rules29
1 files changed, 16 insertions, 13 deletions
diff --git a/debian/rules b/debian/rules
index 6588912e..e4dc420a 100755
--- a/debian/rules
+++ b/debian/rules
@@ -7,8 +7,6 @@ include /usr/share/dpatch/dpatch.make
COQPREF=$(CURDIR)/debian/tmp
ADDPREF=COQINSTALLPREFIX=$(COQPREF)
-MAKEQ=$(MAKE) -q
-
CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man \
--emacslib /usr/share/emacs/site-lisp/coq --reals all
@@ -28,17 +26,22 @@ build: patch-stamp configure-stamp build-stamp
build-stamp:
dh_testdir
if grep -q BEST=opt config/Makefile; \
- then $(MAKE) world \
- || (echo WARNING: NATIVE CODE COMPILATION FAILED \
- && echo Trying to build coq in bytecode instead \
- && $(MAKE) archclean clean \
- && $(MAKE) BEST=byte world \
- && echo NATIVE CODE COMPILATION FAILED \
- && echo Coq was built in bytecode instead); \
- else $(MAKE) world; \
- fi
- touch test-suite/success/debian.v8
- $(MAKE) check
+ then \
+ export BEST=opt; \
+ $(MAKE) world \
+ || (echo WARNING: NATIVE CODE COMPILATION FAILED \
+ && echo Trying to build coq in bytecode instead \
+ && export BEST=byte \
+ && $(MAKE) archclean clean \
+ && $(MAKE) BEST=byte world \
+ && echo NATIVE CODE COMPILATION FAILED \
+ && echo Coq was built in bytecode instead); \
+ else \
+ export BEST=byte; \
+ $(MAKE) world; \
+ fi; \
+ touch test-suite/success/debian.v8; \
+ $(MAKE) BEST=$$BEST check
touch build-stamp
clean: unpatch