# HG changeset patch
# User wenzelm
# Date 1421699087 -3600
# Node ID a8bb88ce59dc3d4b5e8b8ce9686b20940d1fdb24
# Parent  0426b53a5d54b15d11bbe31c70233e3fc4ce631b
tuned message;

diff -r 0426b53a5d54 -r a8bb88ce59dc src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Mon Jan 19 21:15:30 2015 +0100
+++ b/src/Pure/General/graph_display.ML	Mon Jan 19 21:24:47 2015 +0100
@@ -88,7 +88,7 @@
         YXML.output_markup_elem
           (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
       val _ =
-        writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "new graph" ^ en);
+        writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
 
       val ((bg1, bg2), en) =
         YXML.output_markup_elem