Extend the test suite (with coq 8.12.1 and coq-native)

* Follow-up of math-comp@52988b6 * Now possible after the merge of coq/opam#1835
thery · Jan 3, 2023 · 4cc5391 · 4cc5391
1 parent 4f18dc2
commit 4cc5391
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -35,9 +35,7 @@ jobs:
               . configure  # sourcing mandatory
               coq_version
             endGroup
-            # Note: Replace with "if coq_native_compiler"
-            # to also test with Coq 8.12.1+
-            if coq_native_compiler_default; then
+            if coq_native_compiler; then
               startGroup "Workaround permission issue"
                 sudo chown -R coq:coq .  # <--(§)
               endGroup

diff --git a/configure b/configure
@@ -36,9 +36,7 @@ coq_native_compiler() {
 }
 
 main() {
-    # Note: Replace with "if coq_native_compiler"
-    # to also test with Coq 8.12.1+
-    if coq_native_compiler_default; then
+    if coq_native_compiler; then
         echo 'coq-native support enabled!' >&2
         sed -e 's/;coq-native-disabled; \?//' "$dir/src/dune.in" > "$dir/src/dune"
     else