aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Michael Soegtrop <michael.soegtrop@intel.com>2018-06-28 15:00:54 +0200
committerGravatar Michael Soegtrop <michael.soegtrop@intel.com>2018-06-28 15:00:54 +0200
commitaa44f98e8a8586f4bc1b96a69f6f39c1f20bed5e (patch)
tree47f309da85f77e246fb6afe60a04cde84d7a6129 /dev
parent25271d6be165172c8ed8d059f545f5a1616f8f0f (diff)
parentb49deb31595cecf6eff3efa432f044c403a10097 (diff)
Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/makecoq_mingw.sh10
1 files changed, 7 insertions, 3 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index a4e60744f..94e90bf4f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1437,12 +1437,16 @@ function make_addon_equations {
}
function make_addons {
- if [ -n "${GITLAB_CI}" ]; then
+ if [ -n "$GITLAB_CI" ]; then
export CI_BRANCH="$CI_COMMIT_REF_NAME"
- if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
- then
+ if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+ else
+ export CI_PULL_REQUEST=""
fi
+ else
+ export CI_BRANCH=""
+ export CI_PULL_REQUEST=""
fi
. /build/ci-basic-overlay.sh
for overlay in /build/user-overlays/*.sh; do