# HG changeset patch
# User wenzelm
# Date 1553274292 -3600
# Node ID dbc2426a600db5a43ca8e7e22e089cf7a88bb12f
# Parent  a7a0115061ec6b74e32218d08e83d67fd6678e6b
workaround for the sake of Windows;

diff -r a7a0115061ec -r dbc2426a600d src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Fri Mar 22 11:23:17 2019 +0100
+++ b/src/HOL/Library/code_test.ML	Fri Mar 22 18:04:52 2019 +0100
@@ -467,9 +467,9 @@
 
     val compiled_path = Path.append path (Path.basic "test")
     val compile_cmd =
-      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^
+      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
-      File.bash_path code_path ^ " " ^ File.bash_path driver_path
+      File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
 
     val run_cmd = File.bash_path compiled_path
   in
diff -r a7a0115061ec -r dbc2426a600d src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Mar 22 11:23:17 2019 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Mar 22 18:04:52 2019 +0100
@@ -889,7 +889,7 @@
         make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
           (*extension demanded by OCaml compiler*),
         make_command = fn _ =>
-          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
+          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
       evaluation_args = []})
   #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))