From 88773f2520f5a9a4bf1ff68f884a3ebe3e1846fb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Nov 2020 09:38:00 +0100
Subject: [PATCH] add HeapLang to timing instructions

---
 CONTRIBUTING.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 43ffe2770..3296de266 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -88,19 +88,19 @@ or the [examples].  To do this, check out the respective project and change its
 build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.9.0   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
+    OPAM_PINS: "coq version 8.9.0   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature   coq-iris-heap-lang.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#yourname/feature"
   tags:
   - fp-timing
 ```
 You will have to adjust this a bit: you should use the same Coq version as
 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.  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.
+checking its `.gitlab-ci.yml`.  You will also have to adjust the Iris branch
+being used, which is determined after the `#` in `OPAM_PINS`.  If the repo you
+are testing does not need HeapLang, you can remove the `coq-iris-heap-lang` part
+of `OPAM_PINS`.  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