--- 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 =