tuned;
authorwenzelm
Sun, 20 May 2018 15:05:17 +0200
changeset 68227 b95a43d8b826
parent 68226 5ce62512de35
child 68228 326f4bcc5abc
tuned;
src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 20 12:29:51 2018 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 20 15:05:17 2018 +0200
@@ -99,7 +99,7 @@
       then
         let
           val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
-          val _ = File.open_output (fn out => List.app (File.output out) output) path;
+          val _ = File.write_list path output;
         in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
       else
         (case Markup.dest_loading_theory props of