author | wenzelm |
Wed, 26 Jul 2023 15:42:13 +0200 | |
changeset 78468 | 33bc244eafdb |
parent 78467 | ab9cc7cda0ec |
child 78469 | 53b59fa42696 |
child 78471 | 7c3d681f11d4 |
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Jul 26 15:06:06 2023 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Wed Jul 26 15:42:13 2023 +0200 @@ -48,7 +48,7 @@ val new_output = if (restriction.isEmpty || restriction.get.contains(command)) - Rendering.output_messages(results, true) + Rendering.output_messages(results, JEdit_Options.output_state()) else current_output if (current_output != new_output) {