changeset 65512 | 9fd620f2fa7d |
parent 65361 | ecefb68dc21d |
child 65922 | d2f19f05c0e9 |
--- a/src/Tools/VSCode/src/server.scala Wed Apr 19 16:24:59 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Wed Apr 19 16:25:26 2017 +0200 @@ -225,7 +225,8 @@ } } - val session_base = Sessions.session_base(options, session_name, session_dirs) + val session_base = + Sessions.session_base(options, session_name, dirs = session_dirs, all_known = true) val resources = new VSCode_Resources(options, session_base, log) { override def commit(change: Session.Change): Unit =