diff options
| author | Théo Zimmermann | 2018-10-08 17:28:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-08 17:28:46 +0200 |
| commit | 2de0af56b813f2004261eb15fe22586105f3c886 (patch) | |
| tree | b0d58e179c8637a2a1a19f60fe4028a8b189d51d /.gitlab-ci.yml | |
| parent | 22e7ae8f9f5d673fd552c30b7709b948bc8f68a5 (diff) | |
| parent | edaf8d0a34993ac5fab373128a27417a620643d4 (diff) | |
Merge PR #8657: [dune] Refactor files following advice from upstream.
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 118482273d..18f515da24 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -241,7 +241,7 @@ pkg:opam: script: - set -e - opam pin add coq . - - opam pin add coqide ide + - opam pin add coqide . - set +e variables: OPAM_SWITCH: edge |