diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 08:42:30 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-18 08:42:30 +0000 |
| commit | 2f100c8cddd5b81aa26fc5db565e28b8e6c12713 (patch) | |
| tree | 5911ba00f963484a770ac9627409f2dcec2972eb | |
| parent | 04c838a604255c8b79425b731daa006047275da5 (diff) | |
Working bytecode fallback.
| -rw-r--r-- | debian/compat | 2 | ||||
| -rwxr-xr-x | debian/rules | 8 |
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 \ |