# HG changeset patch # User wenzelm # Date 1439900909 -7200 # Node ID ad3c5eb9e348da570a0bd2743eaba87e5ec007fe # Parent 49c797cb9f4694f63ff131cce9807f7b62254af6 proper platform path for initial load; diff -r 49c797cb9f46 -r ad3c5eb9e348 lib/scripts/run-polyml-5.5.3 --- a/lib/scripts/run-polyml-5.5.3 Tue Aug 18 14:07:27 2015 +0200 +++ b/lib/scripts/run-polyml-5.5.3 Tue Aug 18 14:28:29 2015 +0200 @@ -52,7 +52,15 @@ esac else check_file "$INFILE" - INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));" + case "$ML_PLATFORM" in + *-windows) + PLATFORM_INFILE="$(jvmpath -m "$INFILE")" + ;; + *) + PLATFORM_INFILE="$INFILE" + ;; + esac + INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));" EXIT="" fi