# HG changeset patch
# User wenzelm
# Date 1569768269 -7200
# Node ID 5006ca9aadbba3eb68792c71c9fc7e97ee4c39f8
# Parent  87beb7fb0cc691e365062f8dadd0d94862e91623
tuned message;

diff -r 87beb7fb0cc6 -r 5006ca9aadbb src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 29 13:29:10 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 29 16:44:29 2019 +0200
@@ -302,7 +302,7 @@
           Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
             val clean_theories = use_theories_state.change_result(_.clean_theories)
             if (clean_theories.nonEmpty) {
-              progress.echo("Removing " + clean_theories.length)
+              progress.echo("Removing " + clean_theories.length + " theories")
               resources.clean_theories(session, id, clean_theories)
             }
           }