From 47700fa340c2049f3a4af8f16c2f5f8b23a6341e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 5 Jul 2017 11:16:02 +0200
Subject: Add a -ignore-coq-version flag to configure
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 configure | 12 ++++++++++--
 1 file 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."
-- 
cgit