src/Pure/Build/store.scala
changeset 80128 2fe244c4bb01
parent 80123 7e4c3bb3d062
--- a/src/Pure/Build/store.scala	Wed Apr 17 15:04:27 2024 +0200
+++ b/src/Pure/Build/store.scala	Wed Apr 17 21:20:31 2024 +0200
@@ -485,9 +485,9 @@
   def check_output(
     database_server: Option[SQL.Database],
     name: String,
-    session_options: Options,
     sources_shasum: SHA1.Shasum,
     input_shasum: SHA1.Shasum,
+    build_thorough: Boolean = false,
     fresh_build: Boolean = false,
     store_heap: Boolean = false
   ): (Boolean, SHA1.Shasum) = {
@@ -500,7 +500,7 @@
           val current =
             !fresh_build &&
               build.ok &&
-              Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+              Sessions.eq_sources(build_thorough, build.sources, sources_shasum) &&
               build.input_heaps == input_shasum &&
               build.output_heap == output_shasum &&
               !(store_heap && output_shasum.is_empty)