From 3f4d6464ee2463291b5d6b65d8c40d6430c3c360 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 9 Dec 2020 17:44:03 +0100
Subject: [ci] simplify overlay scripts

---
 dev/ci/user-overlays/README.md | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'dev/ci/user-overlays')

diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 3f9ad5e878..14ee5e4199 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -21,14 +21,11 @@ and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 Example: `13128-SkySkimmer-noinstance.sh` containing
 
 ```
-if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then
-
-    overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance
-
-fi
+overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128
 ```
 
-(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
+See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of
+the `overlay` function.
 
 ### Branching conventions
 
-- 
cgit v1.2.3