always explore all sessions;
authorwenzelm
Wed, 19 Apr 2017 16:25:26 +0200
changeset 65512 9fd620f2fa7d
parent 65511 ea42dfd95ec8
child 65513 587433a18053
always explore all sessions;
src/Tools/VSCode/src/server.scala
--- 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 =