avoid legacy warnings in "test_code check in OCaml";
authorwenzelm
Fri, 17 Jan 2025 23:15:47 +0100
changeset 81870 a4c0f9d12440
parent 81869 24ef42cab7d6
child 81873 e4ff4a4ee4ec
avoid legacy warnings in "test_code check in OCaml";
src/HOL/Library/code_test.ML
src/Tools/Code/code_ml.ML
--- a/src/HOL/Library/code_test.ML	Fri Jan 17 23:10:39 2025 +0100
+++ b/src/HOL/Library/code_test.ML	Fri Jan 17 23:15:47 2025 +0100
@@ -426,7 +426,7 @@
     val _ = List.app (File.write code_path o snd) code_files
     val _ = File.write driver_path driver
     val cmd =
-      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
+      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w -p-u -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
       File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
   in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end
--- a/src/Tools/Code/code_ml.ML	Fri Jan 17 23:10:39 2025 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Jan 17 23:15:47 2025 +0100
@@ -886,7 +886,7 @@
         make_destination = fn p => p + Path.explode "ROOT.ml"
           (*extension demanded by OCaml compiler*),
         make_command = fn _ =>
-          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
+          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w -p-u -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))]))