# HG changeset patch
# User wenzelm
# Date 1492611926 -7200
# Node ID 9fd620f2fa7db10b1578eeb18861754bae2efa55
# Parent  ea42dfd95ec83b11608812bf6e3c13c3a7506b68
always explore all sessions;

diff -r ea42dfd95ec8 -r 9fd620f2fa7d 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 =