# HG changeset patch # User wenzelm # Date 1677600759 -3600 # Node ID f37b02353519ff58d03472d0e3416fe43422ebad # Parent 149cc77f7348b6f4bf5d86926490db45b6aa9ea4 simplified somewhat pointless error message (see also 0189fe0f6452); diff -r 149cc77f7348 -r f37b02353519 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Tue Feb 28 16:25:23 2023 +0100 +++ b/src/Pure/ML/ml_process.scala Tue Feb 28 17:12:39 2023 +0100 @@ -61,10 +61,7 @@ else List( "(PolyML.SaveState.loadHierarchy " + - ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + - "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + - ML_Syntax.print_string_bytes(": " + logic_name + "\n") + - "); OS.Process.exit OS.Process.failure)") + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)") val eval_modes = if (modes.isEmpty) Nil