# HG changeset patch
# User wenzelm
# Date 1678548099 -3600
# Node ID 0212956aaf7374c6c7f79d28e44d872d54b72cac
# Parent  58b7f3fb73cbd3aece584bf8955434a3e0b75bcb
more accurate shasum_meta_info;

diff -r 58b7f3fb73cb -r 0212956aaf73 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(