tuned;
authorwenzelm
Tue, 28 Feb 2023 17:16:50 +0100
changeset 77413 1b56b5471c7d
parent 77412 f37b02353519
child 77414 0d5994eef9e6
tuned;
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Feb 28 17:12:39 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Feb 28 17:16:50 2023 +0100
@@ -58,10 +58,11 @@
           "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
           "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
       }
-      else
+      else {
         List(
           "(PolyML.SaveState.loadHierarchy " +
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)")
+      }
 
     val eval_modes =
       if (modes.isEmpty) Nil