Skip to content
Snippets Groups Projects
Commit 1d93f617 authored by Ralf Jung's avatar Ralf Jung
Browse files

emphasize picking the right job name

parent 14eb9f85
No related branches found
No related tags found
No related merge requests found
......@@ -61,7 +61,10 @@ whatever the master branch uses for its timing job, which you can determine by
checking its `.gitlab-ci.yml`. If you change the Coq version, remember to do it
in both places (`OPAM_PINS` and `TIMING_CONF`). You will also have to adjust
the Iris branch being used, which is determined after the `#` in `OPAM_PINS`.
If you are in doubt, ask on Mattermost *before* pushing your branch.
If you are in doubt, ask on Mattermost *before* pushing your branch. Please
double-check that the job name is `build-iris.dev` to avoid polluting the caches
of regular CI builds! This way, you are going to share the cache with the
nightly builds, which is fine.
Once you are confident with your CI configuration, push this to a new branch
whose name starts with `ci/`. It should usually be of the form
......
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