aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-07-05 11:16:02 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2017-07-05 11:16:02 +0200
commit47700fa340c2049f3a4af8f16c2f5f8b23a6341e (patch)
tree1fc9fc41d694180b2d5048a3c97cdc3652da54db
parent01bac827fe4731155e5e8f9f5e9702a6c4a2a128 (diff)
downloadcompcert-kvx-47700fa340c2049f3a4af8f16c2f5f8b23a6341e.tar.gz
compcert-kvx-47700fa340c2049f3a4af8f16c2f5f8b23a6341e.zip
Add a -ignore-coq-version flag to configure
Pull request #188 from Maxime Dénès. This flag makes it easier for the Coq people to test CompCert with in-development versions of Coq.
-rwxr-xr-xconfigure12
1 files changed, 10 insertions, 2 deletions
diff --git a/configure b/configure
index 43109e04..53346109 100755
--- a/configure
+++ b/configure
@@ -21,6 +21,7 @@ has_runtime_lib=true
has_standard_headers=true
clightgen=false
responsefile="gnu"
+ignore_coq_version=false
usage='Usage: ./configure [options] target
@@ -69,6 +70,7 @@ Options:
-no-runtime-lib Do not compile nor install the runtime support library
-no-standard-headers Do not install nor use the standard .h headers
-clightgen Also compile the clightgen tool
+ -ignore-coq-version Accept touse experimental or unsupported versions of Coq
'
@@ -93,6 +95,8 @@ while : ; do
has_standard_headers=false;;
-clightgen)
clightgen=true;;
+ -ignore-coq-version|--ignore-coq-version)
+ ignore_coq_version=true;;
*)
if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
target="$1";;
@@ -434,8 +438,12 @@ case "$coq_ver" in
echo "version $coq_ver -- good!";;
?.*)
echo "version $coq_ver -- UNSUPPORTED"
- echo "Error: CompCert requires Coq version 8.6."
- missingtools=true;;
+ if $ignore_coq_version; then
+ echo "Warning: this version of Coq is unsupported, proceed at your own risks."
+ else
+ echo "Error: CompCert requires Coq version 8.6."
+ missingtools=true
+ fi;;
*)
echo "NOT FOUND"
echo "Error: make sure Coq version 8.6 is installed."