author | wenzelm |
Wed, 14 Jun 2017 11:32:47 +0200 | |
changeset 66090 | 5e1c1b366ac3 |
parent 66086 | 3f7067ba5df3 |
child 66091 | 0a91f2d976c1 |
--- a/src/Tools/VSCode/src/protocol.scala Tue Jun 13 22:39:57 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Wed Jun 14 11:32:47 2017 +0200 @@ -462,8 +462,8 @@ object Dynamic_Output { - def apply(body: String): JSON.T = - Notification("PIDE/dynamic_output", Map("content" -> body)) + def apply(content: String): JSON.T = + Notification("PIDE/dynamic_output", Map("content" -> content)) }