# HG changeset patch
# User wenzelm
# Date 1637148487 -3600
# Node ID d540c36cd0d27b60c1e5facb45965ef2d73db627
# Parent  48fda7ee19731755a95e2ba26037c0ea5c9c64cd
tuned (see also e0d1d9203275);

diff -r 48fda7ee1973 -r d540c36cd0d2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 17 12:10:48 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 17 12:28:07 2021 +0100
@@ -781,8 +781,7 @@
         else {
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.dir_selected || select_session(name) ||
-              graph.get_node(name).groups.exists(select_group)
+            if info.dir_selected || select_session(name) || info.groups.exists(select_group)
           } yield name).toList
         }