# HG changeset patch
# User kleing
# Date 1690376766 -7200
# Node ID ab9cc7cda0ecfb4592637f68d215071411b10f5c
# Parent  1a68cd0c57d331ee32bc7dc1278fd9f459882e83
output panel: don't discard already filtered messages

diff -r 1a68cd0c57d3 -r ab9cc7cda0ec src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Jul 26 13:09:20 2023 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Jul 26 15:06:06 2023 +0200
@@ -48,7 +48,7 @@
 
       val new_output =
         if (restriction.isEmpty || restriction.get.contains(command))
-          Rendering.output_messages(results, JEdit_Options.output_state())
+          Rendering.output_messages(results, true)
         else current_output
 
       if (current_output != new_output) {