# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1738956712 -3600
# Node ID 9b4e021cfd08684359c05e463fc3f7649291b88d
# Parent  28ef95b041f099e5adb485ec12396a0af4a6b055
clarified;

diff -r 28ef95b041f0 -r 9b4e021cfd08 src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 20:30:13 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 20:31:52 2025 +0100
@@ -59,9 +59,9 @@
       meta_info ::: head_digest ::: source_digest
     }
 
-    def get_digest: SHA1.Digest =
+    def get_digest(file: Path = output_file): SHA1.Digest =
       Exn.capture {
-        val html = HTML.parse_document(File.read(output_file))
+        val html = HTML.parse_document(File.read(file))
         val elem = html.head.getElementsByTag("meta").attr("name", "shasum")
         Library.the_single(elem.eachAttr("content").asScala.toList)
       } match {
@@ -71,7 +71,7 @@
 
     def build_html(progress: Progress = new Progress): String = {
       val digest = sources_shasum.digest
-      if (digest == get_digest) File.read(output_file)
+      if (digest == get_digest()) File.read(output_file)
       else {
         progress.echo("Building web application " + output_file.absolute + " ...")