lib/scripts/getsettings
changeset 67099 3345d53e7c58
parent 62588 cd266473b81b
child 68012 6d38b4fd872e
--- a/lib/scripts/getsettings	Mon Nov 27 16:07:49 2017 +0100
+++ b/lib/scripts/getsettings	Mon Nov 27 15:10:50 2017 +0100
@@ -85,6 +85,13 @@
   chmod $(umask -S) "$ISABELLE_HOME_USER"
 fi
 
+#POLYML_EXE
+if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
+  POLYML_EXE="$ML_HOME/poly.exe"
+else
+  POLYML_EXE="$ML_HOME/poly"
+fi
+
 #ML system identifier
 if [ -z "$ML_PLATFORM" ]; then
   ML_IDENTIFIER="$ML_SYSTEM"