disable name mangling test for now, it is incompatible with using the string_ident feature

5e5446b0 · Ralf Jung · fe2b525c · 5e5446b0
Commit 5e5446b0 authored 3 years ago by Ralf Jung
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -31,7 +31,7 @@ build-coq.dev:
  <<: *template
  variables:
    OPAM_PINS: "coq version dev"
-    MANGLE_NAMES: "1"
+    #MANGLE_NAMES: "1" name mangling causes issues with string_ident

 build-coq.8.13.1:
  <<: *template