src/Pure/build
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