# HG changeset patch
# User wenzelm
# Date 1459936207 -7200
# Node ID 108630498c0055243345de758034111b493c45f1
# Parent  66494de0aafe48e29c15c4739d6c6f055d3ee720
more uniform cleanup (via ML_Process in Scala);

diff -r 66494de0aafe -r 108630498c00 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Wed Apr 06 11:44:34 2016 +0200
+++ b/src/Pure/System/options.ML	Wed Apr 06 11:50:07 2016 +0200
@@ -215,9 +215,7 @@
   | name =>
       let val path = Path.explode name in
         (case try File.read path of
-          SOME s =>
-            (set_default (decode (YXML.parse_body s));
-             if default_bool "ML_system_bootstrap" then () else ignore (try File.rm path))
+          SOME s => set_default (decode (YXML.parse_body s))
         | NONE => ())
       end);