# HG changeset patch
# User wenzelm
# Date 1454584287 -3600
# Node ID 7afbd7fc32fd55782cc2b0ed4a1120675e8792f8
# Parent  338bdbf14e31aa0ed3a2e155dcdabb71a328a59a
recovered handle_resize from 5922db0430f1;

diff -r 338bdbf14e31 -r 7afbd7fc32fd src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Feb 01 19:57:58 2016 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Feb 04 12:11:27 2016 +0100
@@ -129,6 +129,7 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
+          handle_resize()
           output_state_button.selected = output_state
           handle_update(do_update, None)
         }