diff options
| author | Michael Soegtrop | 2018-11-07 12:49:45 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2018-11-07 12:49:45 +0100 |
| commit | 14c55444b3bd574f77b4443916c55f8f102414b6 (patch) | |
| tree | bb834b71ca67746a237e2c142aaa362edfaa74bd /dev | |
| parent | ddce2d5b3ace700da602168da4e6bde7cd04e076 (diff) | |
| parent | 4e9e7b4f7ccf54d573ba890ee995ce0ab7a3fc48 (diff) | |
Merge PR #8918: Fix overlays on Windows CI
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c3d895784e..71207bb040 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -434,7 +434,7 @@ function build_prep_overlay { # ------------------------------------------------------------------------------ function load_overlay_data { - if [ -n "${GITLAB_CI+}" ]; then + if [ -n "${GITLAB_CI-}" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" |