# 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(