| changeset 59440 | 07e3c15cb10c |
| parent 59245 | be4180f3c236 |
| child 66823 | f529719cc47d |
--- a/src/Pure/General/graph_display.scala Sun Jan 25 15:40:28 2015 +0100 +++ b/src/Pure/General/graph_display.scala Sun Jan 25 17:17:37 2015 +0100 @@ -10,7 +10,7 @@ { /* graph entries */ - type Entry = ((String, (String, XML.Body)), List[String]) + type Entry = ((String, (String, XML.Body)), List[String]) // ident, name, content, parents /* graph structure */