# HG changeset patch
# User wenzelm
# Date 1670927271 -3600
# Node ID 76ee2762c69eb1934fdc712d285b975310298fa1
# Parent  95c258c0753cbe443021ee140cc4bab94aa67a5b
tuned;

diff -r 95c258c0753c -r 76ee2762c69e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Dec 13 11:25:26 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 13 11:27:51 2022 +0100
@@ -1125,12 +1125,6 @@
     val key: JFile = path.canonical_file
     def dir: Path = path.dir
 
-    def || (that: Root_File): Root_File = {
-      require(key == that.key)
-      val select1 = select || that.select
-      if (select1 == select) this else copy(select = select1)
-    }
-
     lazy val entries: List[Entry] = Parsers.parse_root(path)
   }
 
@@ -1177,7 +1171,8 @@
           seen_roots += (root.key -> (root, next_root))
           next_root += 1
         case Some((root0, next0)) =>
-          seen_roots += (root0.key -> (root0 || root, next0))
+          val root1 = root0.copy(select = root0.select || root.select)
+          seen_roots += (root0.key -> (root1, next0))
       }
     }
     seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1)