# HG changeset patch
# User wenzelm
# Date 1495445682 -7200
# Node ID f02a1289e2c6e5a24c7cf719af73c8a2d08ff376
# Parent  94b0da1b242ed449fd12de71a05fe1e543d5075f
proper File.platform_path for poly on Windows;

diff -r 94b0da1b242e -r f02a1289e2c6 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon May 22 00:23:25 2017 +0200
+++ b/src/HOL/Library/code_test.ML	Mon May 22 11:34:42 2017 +0200
@@ -341,8 +341,9 @@
       "    ()\n" ^
       "  end;\n"
     val cmd =
-      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
-      Path.implode driver_path ^ "\\\"; main ();\" | \"$ML_HOME/poly\""
+      "\"$ML_HOME/poly\" --use " ^ Bash.string (File.platform_path code_path) ^
+      " --use " ^ Bash.string (File.platform_path driver_path) ^
+      " --eval " ^ Bash.string "main ()"
   in
     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   end