summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 08:42:30 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 08:42:30 +0000
commit2f100c8cddd5b81aa26fc5db565e28b8e6c12713 (patch)
tree5911ba00f963484a770ac9627409f2dcec2972eb /debian
parent04c838a604255c8b79425b731daa006047275da5 (diff)
Working bytecode fallback.
Diffstat (limited to 'debian')
-rw-r--r--debian/compat2
-rwxr-xr-xdebian/rules8
2 files changed, 2 insertions, 8 deletions
diff --git a/debian/compat b/debian/compat
index bf0d87ab..b8626c4c 100644
--- a/debian/compat
+++ b/debian/compat
@@ -1 +1 @@
-4 \ No newline at end of file
+4
diff --git a/debian/rules b/debian/rules
index 27b02b62..6588912e 100755
--- a/debian/rules
+++ b/debian/rules
@@ -27,14 +27,8 @@ configure-stamp: patch
build: patch-stamp configure-stamp build-stamp
build-stamp:
dh_testdir
-# if grep -q BEST=opt config/Makefile; \
-# then ($(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
-# && $(MAKEQ) bin/coqmktop bin/coqc bin/coqtop.byte \
-# && $(MAKEQ) bin/coqtop.opt bin/coqtop \
-# && $(MAKEQ) states \
-# && $(MAKEQ) world ) \
if grep -q BEST=opt config/Makefile; \
- then ($(MAKE) world) \
+ then $(MAKE) world \
|| (echo WARNING: NATIVE CODE COMPILATION FAILED \
&& echo Trying to build coq in bytecode instead \
&& $(MAKE) archclean clean \