more accurate shasum_meta_info;
authorwenzelm
Sat, 11 Mar 2023 16:21:39 +0100
changeset 77618 0212956aaf73
parent 77617 58b7f3fb73cb
child 77619 6d0985955872
more accurate shasum_meta_info;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sat Mar 11 16:11:26 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Mar 11 16:21:39 2023 +0100
@@ -301,9 +301,12 @@
       val root_name1 = "root_" + doc.name
       val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
 
+      val document_prefs = latex_output.options.make_prefs(filter = _.for_document)
+
       val meta_info =
         SHA1.shasum_meta_info(
-          SHA1.digest(List(doc.print, document_logo.toString, document_build).toString))
+          SHA1.digest(
+            List(doc.print, document_logo.toString, document_build, document_prefs).toString))
 
       val manifest =
         SHA1.shasum_sorted(