src/Tools/VSCode/src/protocol.scala
changeset 65979 c208fcf369b7
parent 65977 c51b74be23b6
child 65983 d8c5603c1732
--- a/src/Tools/VSCode/src/protocol.scala	Tue May 30 22:09:37 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Tue May 30 22:14:00 2017 +0200
@@ -461,7 +461,7 @@
   object Dynamic_Output
   {
     def apply(body: String): JSON.T =
-      Notification("PIDE/dynamic_output", Map("body" -> body))
+      Notification("PIDE/dynamic_output", Map("content" -> body))
   }