summaryrefslogtreecommitdiff
path: root/debian/rules
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-17 23:41:17 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-17 23:41:17 +0000
commit04c838a604255c8b79425b731daa006047275da5 (patch)
treec3f0a5f3d2ef3e9559067d7ab95ed4fb25720443 /debian/rules
parent97cc3f9bb7f50a9d38494b3a4c5fa78384f1cf79 (diff)
Try to build in opt, ready for dpatch, manpages added (but not used yet).
Diffstat (limited to 'debian/rules')
-rwxr-xr-xdebian/rules24
1 files changed, 14 insertions, 10 deletions
diff --git a/debian/rules b/debian/rules
index beb3d42c..27b02b62 100755
--- a/debian/rules
+++ b/debian/rules
@@ -1,6 +1,9 @@
#!/usr/bin/make -f
# debian/rules for coq
+# We want to use dpatch.
+include /usr/share/dpatch/dpatch.make
+
COQPREF=$(CURDIR)/debian/tmp
ADDPREF=COQINSTALLPREFIX=$(COQPREF)
@@ -21,29 +24,30 @@ configure-stamp: patch
if [ `arch` = ppc ] ; then ./configure $(CONFIGUREOPTS) ; fi
touch configure-stamp
-build: configure-stamp build-stamp
+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 ($(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 ) \
- || (echo WARNING: NATIVE CODE COMPILATION FAILED \
- && echo Trying to build coq in bytecode \
+ 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
- $(MAKE) world
touch test-suite/success/debian.v8
$(MAKE) check
touch build-stamp
-clean:
+clean: unpatch
dh_testdir
dh_testroot
rm -f build-stamp configure-stamp