# HG changeset patch
# User wenzelm
# Date 1511797472 -3600
# Node ID 60126738b2d0146a69e838795befefce317e5710
# Parent  c7694d51c2781764fcfad3882117d9dbad259930
prefer formal $POLYML_EXE;

diff -r c7694d51c278 -r 60126738b2d0 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Mon Nov 27 16:18:29 2017 +0100
+++ b/src/HOL/Library/code_test.ML	Mon Nov 27 16:44:32 2017 +0100
@@ -343,7 +343,7 @@
       "    ()\n" ^
       "  end;\n"
     val cmd =
-      "\"$ML_HOME/poly\" --use " ^ Bash.string (File.platform_path code_path) ^
+      "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
       " --use " ^ Bash.string (File.platform_path driver_path) ^
       " --eval " ^ Bash.string "main ()"
   in