src/Pure/Tools/build.scala
changeset 66782 193c31b79a33
parent 66749 0445cfaf6132
child 66822 4642cf4a7ebb
--- a/src/Pure/Tools/build.scala	Sun Oct 08 12:36:00 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 08 12:50:18 2017 +0200
@@ -228,7 +228,7 @@
 
         def save_heap: String =
           "ML_Heap.share_common_data (); ML_Heap.save_child " +
-            ML_Syntax.print_string0(File.platform_path(output))
+            ML_Syntax.print_string_bytes(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
           val resources = new Resources(deps(parent))
@@ -262,7 +262,7 @@
 
           val eval =
             "Command_Line.tool0 (fn () => (" +
-            "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
+            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
             (if (do_output) "; " + save_heap else "") + "));"
 
           val process =