src/Pure/Tools/build.scala
changeset 66782 193c31b79a33
parent 66749 0445cfaf6132
child 66822 4642cf4a7ebb
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 15:37:46 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Oct 08 12:50:18 2017 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4  
     1.5          def save_heap: String =
     1.6            "ML_Heap.share_common_data (); ML_Heap.save_child " +
     1.7 -            ML_Syntax.print_string0(File.platform_path(output))
     1.8 +            ML_Syntax.print_string_bytes(File.platform_path(output))
     1.9  
    1.10          if (pide && !Sessions.is_pure(name)) {
    1.11            val resources = new Resources(deps(parent))
    1.12 @@ -262,7 +262,7 @@
    1.13  
    1.14            val eval =
    1.15              "Command_Line.tool0 (fn () => (" +
    1.16 -            "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    1.17 +            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
    1.18              (if (do_output) "; " + save_heap else "") + "));"
    1.19  
    1.20            val process =