Skip to content
Snippets Groups Projects
Commit 26ca5cff authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Merge branch 'rodolphe/dune' into 'master'

Fix convention in gitlab config.

See merge request !556
parents a016f59a abf21ce7
No related branches found
No related tags found
1 merge request!556Fix convention in gitlab config.
Pipeline #103091 passed
......@@ -72,7 +72,7 @@ build-coq.8.19.0-dune:
<<: *template
<<: *branches_and_mr
variables:
OPAM_PINS: "coq version 8.19.0 dune version 3.15.2"
OPAM_PINS: "coq version 8.19.0 dune version 3.15.2"
MAKE_TARGET: "dune"
# The oldest version runs in MRs, without name mangling.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment