From 4e9e7b4f7ccf54d573ba890ee995ce0ab7a3fc48 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Nov 2018 14:24:42 +0100
Subject: Fix overlays on Windows CI

"${foo+}" is always the empty string
"${foo-}" is "$foo" when foo is set and empty string when it's unset.
---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

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-}"
-- 
cgit v1.2.3