From da2b3f94fb732048b8c4dd013ebe8bb35150f468 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Mon, 20 Jun 2011 10:28:56 -0600 Subject: [PATCH] fix initial panel size so that it doesn't force an enclosing frame to grow --- collects/mred/private/wx/gtk/panel.rkt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/collects/mred/private/wx/gtk/panel.rkt b/collects/mred/private/wx/gtk/panel.rkt index e66e8f99ef..db88e9ec1a 100644 --- a/collects/mred/private/wx/gtk/panel.rkt +++ b/collects/mred/private/wx/gtk/panel.rkt @@ -77,7 +77,7 @@ style label) - (inherit set-size get-gtk) + (inherit get-gtk set-auto-size set-size) (define gtk (as-gtk-allocation (gtk_event_box_new))) (define client-gtk (atomically @@ -92,6 +92,9 @@ [gtk gtk] [extra-gtks (list client-gtk)] [no-show? (memq 'deleted style)]) + + ;; Start with a minimum size: + (set-size 0 0 1 1) (connect-key-and-mouse gtk) (gtk_widget_add_events gtk (bitwise-ior GDK_BUTTON_PRESS_MASK