changeset 52083 | f852d08376f9 |
parent 52054 | eaf17514aabd |
child 60962 | faa452d8e265 |
--- a/src/Pure/build Mon May 20 14:04:21 2013 +0200 +++ b/src/Pure/build Mon May 20 15:42:14 2013 +0200 @@ -80,6 +80,7 @@ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -e "Command_Line.tool0 Session.finish;" \ + -e "Options.reset_default ();" \ -q -w RAW_ML_SYSTEM "$OUTPUT" fi fi