# HG changeset patch
# User wenzelm
# Date 1507627475 -7200
# Node ID 5baca4c94737a2b828c0eb985546c5fd58a9b915
# Parent  3c936ebebc23c50526d400bbe7061484049393ae
tuned signature;

diff -r 3c936ebebc23 -r 5baca4c94737 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 10 11:20:02 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 11:24:35 2017 +0200
@@ -355,7 +355,7 @@
   sealed case class Info(
     name: String,
     chapter: String,
-    select: Boolean,
+    dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
@@ -425,7 +425,7 @@
           val select = sessions.toSet ++ graph.all_succs(base_sessions)
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
+            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
       }.filterNot(excluded)