From 2f100c8cddd5b81aa26fc5db565e28b8e6c12713 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Sun, 18 Jul 2004 08:42:30 +0000
Subject: Working bytecode fallback.

---
 debian/rules | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'debian/rules')

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 \
-- 
cgit v1.2.3