Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Sun, 08 Oct 2017 12:50:23 +0200
changeset 66784 df1f43d477f5
parent 66783 bbe87f1b5e5d (diff)
parent 66782 193c31b79a33 (current diff)
child 66789 feb36b73a7f0
merged
--- a/src/HOL/Library/code_test.ML	Sun Oct 08 12:50:18 2017 +0200
+++ b/src/HOL/Library/code_test.ML	Sun Oct 08 12:50:23 2017 +0200
@@ -425,8 +425,8 @@
       "end;"
     val ml_source =
       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
-      "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
-      "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand driver_path)) ^
+      "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
+      "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
       "; Test.main ();"
     val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
   in
isabelle