author | wenzelm |
Sun, 25 Jan 2015 17:17:37 +0100 | |
changeset 59440 | 07e3c15cb10c |
parent 59439 | 397ce0940c44 |
child 59441 | ab2c3597f1d3 |
--- 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 */