# HG changeset patch
# User wenzelm
# Date 1673715132 -3600
# Node ID fd4195298effa2136285b8d709a55f705a96ca0c
# Parent  38e19412cf310f4d0359ad5e7a54d8a72970dbd1
tuned;

diff -r 38e19412cf31 -r fd4195298eff src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 13 19:16:24 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sat Jan 14 17:52:12 2023 +0100
@@ -67,14 +67,14 @@
         case XML.Wrapped_Elem(markup, body1, body2) =>
           val body = if (markup.name == Markup.UPDATE) body1 else body2
           update_xml(lang, body)
-        case XML.Elem(Markup.Language(lang), body) =>
-          if (lang.is_path && path_cartouches) {
+        case XML.Elem(Markup.Language(lang1), body) =>
+          if (lang1.is_path && path_cartouches) {
             Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
               case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
-              case None => update_xml(lang, body)
+              case None => update_xml(lang1, body)
             }
           }
-          else update_xml(lang, body)
+          else update_xml(lang1, body)
         case XML.Elem(_, body) => update_xml(lang, body)
         case t => List(t)
       }