tuned message;
authorwenzelm
Mon, 19 Jan 2015 21:24:47 +0100
changeset 59413 a8bb88ce59dc
parent 59412 0426b53a5d54
child 59414 eb3d8e7b4b21
tuned message;
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