# HG changeset patch
# User wenzelm
# Date 1569841882 -7200
# Node ID 8abda6f6b7002b316e73d4fefc9efa6cede2a0bc
# Parent  9514fdbb8abea1a10a9590582904c09efa5009ce
tuned message;

diff -r 9514fdbb8abe -r 8abda6f6b700 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Sep 30 12:52:16 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 30 13:11:22 2019 +0200
@@ -320,7 +320,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 + " theories")
+              progress.echo("Removing " + clean_theories.length + " theories ...")
               resources.clean_theories(session, id, clean_theories)
             }
           }