prefer formal $POLYML_EXE;
authorwenzelm
Mon Nov 27 16:44:32 2017 +0100 (11 months ago)
changeset 6710160126738b2d0
parent 67100 c7694d51c278
child 67102 411e49edd905
prefer formal $POLYML_EXE;
src/HOL/Library/code_test.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Mon Nov 27 16:18:29 2017 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Mon Nov 27 16:44:32 2017 +0100
     1.3 @@ -343,7 +343,7 @@
     1.4        "    ()\n" ^
     1.5        "  end;\n"
     1.6      val cmd =
     1.7 -      "\"$ML_HOME/poly\" --use " ^ Bash.string (File.platform_path code_path) ^
     1.8 +      "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
     1.9        " --use " ^ Bash.string (File.platform_path driver_path) ^
    1.10        " --eval " ^ Bash.string "main ()"
    1.11    in