author | wenzelm |
Tue, 23 Dec 2014 21:14:44 +0100 | |
changeset 59186 | 45e31a196b57 |
parent 59185 | 08ff767a82bf |
child 59187 | 5a783837b50b |
--- a/src/Pure/PIDE/markup.scala Tue Dec 23 21:04:53 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Dec 23 21:14:44 2014 +0100 @@ -344,8 +344,6 @@ val SERIAL = "serial" val Serial = new Properties.Long(SERIAL) - val MESSAGE = "message" - val INIT = "init" val STATUS = "status" val REPORT = "report"