# HG changeset patch
# User wenzelm
# Date 1526821517 -7200
# Node ID b95a43d8b826f623182d2aa0ffb3583bd37a0714
# Parent  5ce62512de35b675846efe93f81ae4fba16db792
tuned;

diff -r 5ce62512de35 -r b95a43d8b826 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