author | wenzelm |
Wed, 06 Apr 2016 11:50:07 +0200 | |
changeset 62885 | 108630498c00 |
parent 62884 | 66494de0aafe |
child 62886 | 72c475e03e22 |
--- 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);