# HG changeset patch
# User wenzelm
# Date 1674055664 -3600
# Node ID 2342b4cc118f0c5950daf395d759822885d7f02e
# Parent  60b465c4463cfe2574d82484e3e41f42b3b632e4
tuned messages;

diff -r 60b465c4463c -r 2342b4cc118f src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Wed Jan 18 16:22:55 2023 +0100
+++ b/src/Pure/Tools/update.scala	Wed Jan 18 16:27:44 2023 +0100
@@ -95,7 +95,7 @@
         session <- sessions_structure.build_topological_order
         if build_results(session).ok && !exclude(session)
       } {
-        progress.echo("Session " + session + " ...")
+        progress.echo("Updating " + session + " ...")
         val session_options = sessions_structure(session).options
         val proper_session_theory =
           build_results.deps(session).proper_session_theories.map(_.theory).toSet
@@ -118,7 +118,7 @@
               val source1 = XML.content(update_xml(session_options, xml))
               if (source1 != snapshot.node.source) {
                 val path = Path.explode(node_name.node)
-                progress.echo("Updating " + quote(File.standard_path(path)))
+                progress.echo("File " + quote(File.standard_path(path)))
                 File.write(path, source1)
               }
             }