# HG changeset patch
# User wenzelm
# Date 1675460399 -3600
# Node ID 461c078e545fd959a69422dc3f5e2398633d9dc7
# Parent  608668d39689913dfa690ae2657a9770a7206658
no view_document after build: avoid loss of focus, especially in "auto build" mode;

diff -r 608668d39689 -r 461c078e545f src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 21:25:17 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 22:39:59 2023 +0100
@@ -232,7 +232,6 @@
         if (!ok) {
           Document_Editor.write_document(document_session.selection,
             engine.build_document(context, directory, verbose = true))
-          Document_Editor.view_document()
         }
       }
     }