diff --git a/.scripts/bin-install.sh b/.scripts/bin-install.sh index 6ee6a98dd37..cd8571e5140 100755 --- a/.scripts/bin-install.sh +++ b/.scripts/bin-install.sh @@ -1,17 +1,21 @@ #!/bin/bash # This is called by the Makefile *after* an installation into the -# prefix, so we add the rest of the files that go into a binary pacakge. +# prefix, so we add the rest of the files that go into a binary package. set -eu windows () { - [ -v OS ] && [ "$OS" = "Windows_NT" ] + # This seems portable enough and does not trigger an + # undefined variable error (see set -u above) if $OS + # is unset (like in linux/mac). Note: OSX's bash is usually + # old and does not support '[ -v OS ]'. + [[ "${OS:-}" = "Windows_NT" ]] } if [ $# -ne 1 ]; then - echo "Usage: $0 " >&2 - exit 1 + echo "Usage: $0 " >&2 + exit 1 fi PREFIX="$1" diff --git a/.scripts/make_fstar_version.sh b/.scripts/make_fstar_version.sh index d4ebe49b567..e47448b6a36 100755 --- a/.scripts/make_fstar_version.sh +++ b/.scripts/make_fstar_version.sh @@ -1,11 +1,14 @@ #!/usr/bin/env bash +windows () { + [[ "${OS:-}" = "Windows_NT" ]] +} + if [[ -z "$FSTAR_VERSION" ]]; then FSTAR_VERSION=$(head -n 1 version.txt)~dev fi -if [ "$OS" = "Windows_NT" ] -then +if windows; then if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" ] then PLATFORM="Windows_x64" diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh index 1f9b7ec472b..7d37bed1062 100755 --- a/.scripts/mk-package.sh +++ b/.scripts/mk-package.sh @@ -25,7 +25,11 @@ PREFIX="$1" ARCHIVE="$2" windows () { - [ -v OS ] && [ "$OS" = "Windows_NT" ] + # This seems portable enough and does not trigger an + # undefined variable error (see set -u above) if $OS + # is unset (like in linux/mac). Note: OSX's bash is usually + # old and does not support '[ -v OS ]'. + [[ "${OS:-}" = "Windows_NT" ]] } # Computes a (hopefully) sensible default for the current system