# HG changeset patch
# User wenzelm
# Date 1458048618 -3600
# Node ID 1815513a57f1a28b552358533e41cc1d72b67c18
# Parent  6031191a8d9c7d89f4f54e3d51991ffd1b76f5d2
clarified prompt: "ML" usually means Isabelle/ML;

diff -r 6031191a8d9c -r 1815513a57f1 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Mon Mar 14 17:43:17 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Tue Mar 15 14:30:18 2016 +0100
@@ -59,8 +59,8 @@
             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
           else
             "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
-          "PolyML.Compiler.prompt1 := \"ML> \"",
-          "PolyML.Compiler.prompt2 := \"ML# \"")
+          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
+          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
       }
       else Nil