author | wenzelm |
Fri, 03 Feb 2023 22:39:59 +0100 | |
changeset 77189 | 461c078e545f |
parent 77188 | 608668d39689 |
child 77190 | f6ba88f23135 |
--- 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() } } }