# HG changeset patch
# User wenzelm
# Date 1675181296 -3600
# Node ID 2f43be96c713cb7faae57c993be4db45fa8a24fe
# Parent  286fdf0fcc443376f9e37793fa4b531abeba091a
removed unused operation from 3f50b24909df;

diff -r 286fdf0fcc44 -r 2f43be96c713 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:04:02 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:08:16 2023 +0100
@@ -48,8 +48,6 @@
       output_main :::
       (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) :::
       output_more
-
-    def ok: Boolean = !output_body.exists(Protocol.is_error)
   }
 }