diff options
| author | Gaëtan Gilbert | 2020-11-26 15:04:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-26 15:10:07 +0100 |
| commit | ea795d144c59facfcfa1837fdce3ca654b159d58 (patch) | |
| tree | 0763ac903587072464f64e88e77f40c6754c13c7 /dev/ci/README-developers.md | |
| parent | 7f3c46acc937eb9257c29b5881e5a8b17b28cd48 (diff) | |
CI: Use hash of dockerfile in CACHEKEY
Checked by the linter so we don't forget to update it.
Also checked by before_script so we don't run jobs for nothing.
Diffstat (limited to 'dev/ci/README-developers.md')
| -rw-r--r-- | dev/ci/README-developers.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 801e29ac95..f5ca6c495f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -171,7 +171,7 @@ loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) -and [`Dockerfile`](docker/bionic_coq/Dockerfile) +(see comment near it for details). The Docker building job reuses the uploaded image if it is available, but if you wish to save more time you can skip the job by setting |