# HG changeset patch
# User wenzelm
# Date 1710011047 -3600
# Node ID 207762ffc847e113732930f025d8d457daf23d85
# Parent  c69ae2b8987e4b11ee9cc067963ec5c1c9f8daa2
tuned;

diff -r c69ae2b8987e -r 207762ffc847 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Mar 09 19:57:08 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Mar 09 20:04:07 2024 +0100
@@ -86,10 +86,6 @@
   object Sessions {
     type Graph = isabelle.Graph[String, Build_Job.Session_Context]
     val empty: Sessions = new Sessions(Graph.string)
-
-    def update(sessions0: Sessions, sessions1: Sessions): Library.Update =
-      if (sessions0.eq(sessions1)) Library.Update.empty
-      else Library.Update.make(sessions0.data, sessions1.data)
   }
 
   final class Sessions private(val graph: Sessions.Graph) {
@@ -469,7 +465,9 @@
       sessions: Build_Process.Sessions,
       old_sessions: Build_Process.Sessions
     ): Boolean = {
-      val update = Build_Process.Sessions.update(old_sessions, sessions)
+      val update =
+        if (old_sessions.eq(sessions)) Library.Update.empty
+        else Library.Update.make(old_sessions.data, sessions.data)
 
       if (update.deletes) {
         db.execute_statement(