changeset 50503 | 50f141b34bb7 |
parent 50501 | 6f41f1646617 |
child 50543 | 42bbe637be54 |
--- a/src/Pure/PIDE/markup.scala Thu Dec 13 17:46:33 2012 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Dec 13 18:00:24 2012 +0100 @@ -286,7 +286,7 @@ val PADDING_LINE = (PADDING, LINE) val DIALOG = "dialog" - val Result = new Properties.String("result") + val Result = new Properties.String(RESULT) /* protocol message functions */