# HG changeset patch
# User wenzelm
# Date 1737152147 -3600
# Node ID a4c0f9d124403b1a0b51e2b4f6c7383a25c98900
# Parent  24ef42cab7d61a0542dd7ef388d91bd012967f6b
avoid legacy warnings in "test_code check in OCaml";

diff -r 24ef42cab7d6 -r a4c0f9d12440 src/HOL/Library/code_test.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
diff -r 24ef42cab7d6 -r a4c0f9d12440 src/Tools/Code/code_ml.ML
--- 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))]))