From 87af4f4c41878bee5d02ab8560898c56611baa4c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 22 May 2018 12:59:05 +0200 Subject: Relax advice on the name of user-overlays following Gaëtan's suggestion. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit [ci skip] --- dev/ci/user-overlays/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'dev') 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 -- cgit v1.2.3