# 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);