diff options
| -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 \ |