equal
deleted
inserted
replaced
180 PLATFORM_HEAP_FILE="$HEAP_FILE" |
180 PLATFORM_HEAP_FILE="$HEAP_FILE" |
181 ;; |
181 ;; |
182 esac |
182 esac |
183 PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")" |
183 PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")" |
184 FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
184 FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval" |
185 FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success)" |
185 FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)" |
186 fi |
186 fi |
187 |
187 |
188 |
188 |
189 ## prepare tmp directory |
189 ## prepare tmp directory |
190 |
190 |