changeset 65441 | 9425e4d8bdb6 |
parent 65361 | ecefb68dc21d |
child 65452 | 9e9750a7932c |
--- a/src/Tools/VSCode/src/vscode_resources.scala Sat Apr 08 12:47:34 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Apr 08 20:56:41 2017 +0200 @@ -43,7 +43,7 @@ val options: Options, session_base: Sessions.Base, log: Logger = No_Logger) - extends Resources(session_name = "", session_base, log) + extends Resources(session_base, log = log) { private val state = Synchronized(VSCode_Resources.State())