changeset 37121 | 8e51fc35d59f |
parent 36689 | 379f5b1e7f91 |
child 37186 | 349e9223c685 |
--- a/src/Pure/General/markup.scala Tue May 25 22:21:31 2010 +0200 +++ b/src/Pure/General/markup.scala Tue May 25 23:03:13 2010 +0200 @@ -193,7 +193,6 @@ val INIT = "init" val STATUS = "status" val WRITELN = "writeln" - val PRIORITY = "priority" val TRACING = "tracing" val WARNING = "warning" val ERROR = "error"