Merge PR coq#19143: ci-wrapper: fix OSTYPE = darwin check on systems …

…which include version info Reviewed-by: herbelin Co-authored-by: herbelin <[email protected]>
SkySkimmer · Jun 18, 2024 · 8239006 · 8239006
2 parents fcf0a12 + 6705f72
commit 8239006
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
@@ -33,7 +33,8 @@ if [ "$COQ_CI_COLOR" = 1 ] && command -v script > /dev/null; then
     if [ "$CI" ]; then
       export TERM=xterm-color
     fi
-    if [ "$OSTYPE" = darwin ]; then
+    # on some macos systems OSTYPE is just "darwin", on others it's followed by version info
+    if [[ "$OSTYPE" =~ ^darwin ]]; then
         script -q /dev/null bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee "$CI_NAME.log"
     else
         script --quiet --flush --return -c "bash '${DIR}/${CI_SCRIPT}'" /dev/null 2>&1 | tee "$CI_NAME.log"