# HG changeset patch
# User wenzelm
# Date 940969935 -7200
# Node ID e45599caee6ca2b6618c80508c539f6216d8e259
# Parent  82025fe607d3b8b3c1dd00da54b342ffc0c3719a
activate ml_prompts;

diff -r 82025fe607d3 -r e45599caee6c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Oct 26 19:06:52 1999 +0200
+++ b/src/Pure/ROOT.ML	Tue Oct 26 22:32:15 1999 +0200
@@ -81,6 +81,6 @@
 val cd = File.cd o Path.unpack;
 
 print_depth 8;
-(*ml_prompts "ML> " "ML# ";*)
+ml_prompts "ML> " "ML# ";
 
 Session.finish ();