File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -535,14 +535,14 @@ missingtools=false
535535echo " Testing Coq... " | tr -d ' \n'
536536coq_ver=$( ${COQBIN} coqc --print-version 2> /dev/null | tr -d ' \r' | cut -d' ' -f1)
537537case " $coq_ver " in
538- 8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1|9.0.0)
538+ 8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1|9.0.0|9.1.0 )
539539 echo " version $coq_ver -- good!" ;;
540540 ?* )
541541 echo " version $coq_ver -- UNSUPPORTED"
542542 if $ignore_coq_version ; then
543543 echo " Warning: this version of Coq is unsupported, proceed at your own risks."
544544 else
545- echo " Error: CompCert requires a version of Coq between 8.15 and 9.0 "
545+ echo " Error: CompCert requires a version of Coq between 8.15 and 9.1 "
546546 missingtools=true
547547 fi ;;
548548 " " )
You can’t perform that action at this time.
0 commit comments