diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-22 12:59:05 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-24 16:44:46 +0200 |
| commit | 87af4f4c41878bee5d02ab8560898c56611baa4c (patch) | |
| tree | 2d3ff1b238611a2b88b3ea4a655448ea4725945a /dev | |
| parent | c0dd7253faa83d1f3230e57071073df321a5e389 (diff) | |
Relax advice on the name of user-overlays following Gaëtan's suggestion.
[ci skip]
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 3414a8786..8cbe8fc33 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -14,8 +14,9 @@ testing is possible. It changes the value of some variables from The file contains very simple logic to test the pull request number or branch name and apply it only in this case. -The name of your overlay file should be of the form -`five_digit_PR_number-GitHub_handle-branch_name.sh`. +The name of your overlay file should start with a five-digit pull request +number, followed by a dash, anything (for instance your GitHub nickname +and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `00669-maximedenes-ssr-merge.sh` containing |