aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-01-31 14:49:34 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-01-31 14:49:34 +0100
commita882f78c069f7337dd9f4abff117d4df98ef38a6 (patch)
tree389d43d0acb11bfc9a392caffab5bc7c8ebc9795 /configure
parent85b1c4091e13dec13fe03f28e81b256c60f9f7ef (diff)
downloadcompcert-kvx-a882f78c069f7337dd9f4abff117d4df98ef38a6.tar.gz
compcert-kvx-a882f78c069f7337dd9f4abff117d4df98ef38a6.zip
Support Coq 8.15.0
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure4
1 files changed, 2 insertions, 2 deletions
diff --git a/configure b/configure
index 3a4bc622..5ea64a48 100755
--- a/configure
+++ b/configure
@@ -504,14 +504,14 @@ missingtools=false
echo "Testing Coq... " | tr -d '\n'
coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
case "$coq_ver" in
- 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1)
+ 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1|8.15.0)
echo "version $coq_ver -- good!";;
?*)
echo "version $coq_ver -- UNSUPPORTED"
if $ignore_coq_version; then
echo "Warning: this version of Coq is unsupported, proceed at your own risks."
else
- echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.1"
+ echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.15.0"
missingtools=true
fi;;
"")