proper File.platform_path for SML/NJ on Windows;
authorwenzelm
Sun Oct 08 12:42:20 2017 +0200 (3 months ago)
changeset 66783bbe87f1b5e5d
parent 66780 bf54ca580bf2
child 66784 df1f43d477f5
proper File.platform_path for SML/NJ on Windows;
src/HOL/Library/code_test.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Sat Oct 07 20:31:01 2017 +0200
     1.2 +++ b/src/HOL/Library/code_test.ML	Sun Oct 08 12:42:20 2017 +0200
     1.3 @@ -425,8 +425,8 @@
     1.4        "end;"
     1.5      val ml_source =
     1.6        "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
     1.7 -      "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
     1.8 -      "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand driver_path)) ^
     1.9 +      "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
    1.10 +      "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
    1.11        "; Test.main ();"
    1.12      val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
    1.13    in