# HG changeset patch # User wenzelm # Date 1353181676 -3600 # Node ID 6c857312c9f51f2e217ac85ece1cf8b9db983c35 # Parent 11cd86c5af3a7fdefe245a52280f289cf6a8fc50 more portable process exit; diff -r 11cd86c5af3a -r 6c857312c9f5 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Sat Nov 17 20:38:57 2012 +0100 +++ b/src/Tools/Code/code_ml.ML Sat Nov 17 20:47:56 2012 +0100 @@ -833,7 +833,7 @@ check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), make_command = fn _ => - "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => Posix.Process.exit 0w1' Pure" } }) + "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } }) #> Code_Target.add_target (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, check = { env_var = "ISABELLE_OCAML",