# HG changeset patch
# User wenzelm
# Date 1675455917 -3600
# Node ID 608668d39689913dfa690ae2657a9770a7206658
# Parent  628a34f4f7543cfd816db0d08140026489fcb03a
tuned message;

diff -r 628a34f4f754 -r 608668d39689 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 20:47:13 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 21:25:17 2023 +0100
@@ -252,7 +252,7 @@
         val msgs =
           result match {
             case Exn.Res(_) =>
-              List(Protocol.writeln_message("OK"))
+              List(Protocol.writeln_message("DONE"))
             case Exn.Exn(exn: Document_Build.Build_Error) =>
               exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
             case Exn.Exn(exn) =>