# HG changeset patch
# User wenzelm
# Date 1419365684 -3600
# Node ID 45e31a196b5702bee1199f4c288e0f2c67a7c526
# Parent  08ff767a82bf2a1cb23d4ab1986049d4cc21e6fc
unused;

diff -r 08ff767a82bf -r 45e31a196b57 src/Pure/PIDE/markup.scala
--- 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"