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)) }