# HG changeset patch # User wenzelm # Date 1673780828 -3600 # Node ID 7ca7343af00e34905d0ea200420b406b50cdd108 # Parent 5e34a2866edb57897265da7ab179383541e10ff8 clarified names; diff -r 5e34a2866edb -r 7ca7343af00e etc/options --- a/etc/options Sun Jan 15 12:04:08 2023 +0100 +++ b/etc/options Sun Jan 15 12:07:08 2023 +0100 @@ -346,7 +346,7 @@ option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" -option update_cite_commands : bool = false +option update_cite : bool = false -- "update cite commands and antiquotations" diff -r 5e34a2866edb -r 7ca7343af00e src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Sun Jan 15 12:04:08 2023 +0100 +++ b/src/Pure/Tools/update.scala Sun Jan 15 12:07:08 2023 +0100 @@ -13,7 +13,7 @@ def update_xml(options: Options, xml: XML.Body): XML.Body = { val update_path_cartouches = options.bool("update_path_cartouches") - val update_cite_commands = options.bool("update_cite_commands") + val update_cite = options.bool("update_cite") def upd(lang: Markup.Language, ts: XML.Body): XML.Body = ts flatMap { @@ -30,7 +30,7 @@ else upd(lang1, body) case XML.Elem(_, body) => upd(lang, body) case XML.Text(s) - if update_cite_commands && (lang.is_document || lang.is_antiquotation) => + if update_cite && (lang.is_document || lang.is_antiquotation) => List(XML.Text(Bibtex.update_cite(s))) case t => List(t) }