From 82e7e2ef749e4f25af0fa14d27d01d624bb9cbd6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 17 Mar 2019 12:46:57 +0100
Subject: [PATCH] emphasize picking the right job name

---
 CONTRIBUTING.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index cc93349c4..e14c34beb 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -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
-- 
GitLab