# HG changeset patch
# User wenzelm
# Date 1754861715 -7200
# Node ID e06c6ae936809d6c2a7086704195f88ecdf1d3cd
# Parent  98943be486072655cac23d341eb2055a87b59d65
tunes messages;

diff -r 98943be48607 -r e06c6ae93680 src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Sun Aug 10 23:32:06 2025 +0200
+++ b/src/Pure/Build/export.scala	Sun Aug 10 23:35:15 2025 +0200
@@ -296,7 +296,7 @@
     def shutdown(close: Boolean = false): List[String] = {
       consumer.shutdown()
       if (close) db.close()
-      errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
+      errors.value.reverse ::: (if (progress.stopped) List("Session export stopped") else Nil)
     }
   }