lib/scripts/getsettings
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