test with name mangling

4103bc56 · Ralf Jung · cae9ec0f · 4103bc56 · 7ae823c0 · 9028d6c1
Commit 4103bc56 authored Apr 19, 2018 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

.gitlab-ci.yml .gitlab-ci.yml +1 -0

ci ci +1 -1

No files found.
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -30,6 +30,7 @@ build-coq.dev:
  <<: *template
  variables:
    OPAM_PINS: "coq version dev"
+    MANGLE_NAMES: "1"
    VALIDATE: "1"

 build-coq.8.8.0:

--- a/ci @ 7ae823c0
+++ b/ci @ 7ae823c0
-Subproject commit 9028d6c194dff126443a1d19f23a13ac1e8ead3a
+Subproject commit 7ae823c0e476e9e9c576671ed10bcffbbcba0ec5