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"