summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 19:20:54 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 19:20:54 +0000
commit1aa163f8f8c548e69b94188497b72a5c1242edb1 (patch)
tree5cd0dab5e2f033fcf656496a2d2a54118567d813 /debian
parentc806af42e185257ef0f3e0646b3c95c8086ff715 (diff)
Corrected a bug due to a really unexpected bheaviour of make.
Diffstat (limited to 'debian')
-rw-r--r--debian/changelog2
-rwxr-xr-xdebian/rules6
2 files changed, 5 insertions, 3 deletions
diff --git a/debian/changelog b/debian/changelog
index 0f8ef5a2..e020a529 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -2,6 +2,8 @@ coq (8.0pl1-1) unstable; urgency=low
* At least the version without QPL-licensed files is out,
closes: #230356, #250497.
+ * If compilation fails in opt, we try to build in byte (opt does not seem to
+ work on sparc).
-- Samuel Mimram <samuel.mimram@ens-lyon.org> Sun, 18 Jul 2004 01:10:24 +0200
diff --git a/debian/rules b/debian/rules
index 23945313..62c14ed8 100755
--- a/debian/rules
+++ b/debian/rules
@@ -29,7 +29,7 @@ build-stamp:
then \
echo opt > best-stamp; \
$(MAKE) world \
- || (echo WARNING: NATIVE CODE COMPILATION FAILED \
+ || (echo WARNING: NATIVE CODE COMPILATION FAILED \
&& echo Trying to build coq in bytecode instead \
&& echo byte > best-stamp \
&& $(MAKE) archclean clean \
@@ -38,10 +38,10 @@ build-stamp:
&& echo Coq was built in bytecode instead); \
else \
echo byte > best-stamp; \
- $(MAKE) world; \
+ $(MAKE) world; \
fi
touch test-suite/success/debian.v8
- $(MAKE) BEST=$(shell cat best-stamp) check
+ $(MAKE) BEST=`cat best-stamp` check
touch build-stamp
clean: unpatch