changeset 79556 | 0631dfc0db07 |
parent 79059 | ae682b2aab03 |
child 82709 | 1008b8e7c78d |
--- a/lib/scripts/getsettings Tue Jan 30 22:43:10 2024 +0100 +++ b/lib/scripts/getsettings Wed Jan 31 12:43:06 2024 +0100 @@ -94,11 +94,14 @@ fi #POLYML_EXE -if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then - POLYML_EXE="$ML_HOME/poly.exe" -else - POLYML_EXE="$ML_HOME/poly" -fi +case "$ISABELLE_PLATFORM_FAMILY" in + windows*) + POLYML_EXE="$ML_HOME/poly.exe" + ;; + *) + POLYML_EXE="$ML_HOME/poly" + ;; +esac #ML system identifier if [ -z "$ML_PLATFORM" ]; then