author | wenzelm |
Thu, 27 Dec 2018 16:32:19 +0100 | |
changeset 69521 | 0428fd0a13b7 |
parent 69520 | 16779868de1f |
child 69522 | 9457d85204f5 |
--- a/src/Pure/Tools/dump.scala Thu Dec 27 16:56:53 2018 +0100 +++ b/src/Pure/Tools/dump.scala Thu Dec 27 16:32:19 2018 +0100 @@ -39,7 +39,7 @@ override def toString: String = name } - val known_aspects = + val known_aspects: List[Aspect] = List( Aspect("markup", "PIDE markup (YXML format)", { case args =>