src/Pure/Build/build.scala
changeset 80128 2fe244c4bb01
parent 80118 0323cd9fcab9
child 80160 ead20482da9c
--- a/src/Pure/Build/build.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/build.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -210,11 +210,9 @@
                 case Some(db) =>
                   using(db)(store.read_build(_, name)) match {
                     case Some(build) if build.ok =>
-                      val session_options = deps0.sessions_structure(name).options
-                      val session_sources = deps0.sources_shasum(name)
-                      if (Sessions.eq_sources(session_options, build.sources, session_sources)) {
-                        None
-                      }
+                      val sources_shasum = deps0.sources_shasum(name)
+                      val thorough = deps0.sessions_structure(name).build_thorough
+                      if (Sessions.eq_sources(thorough, build.sources, sources_shasum)) None
                       else Some(name)
                     case _ => Some(name)
                   }