From cba890e4cba5857f3891e0f5cd087743529ff062 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Nov 2000 11:22:56 +0000 Subject: [PATCH] Now windows resize well (at least some of them) --- helm/interface/mmlinterface.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index dae8b8738..784c9f4b1 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -588,7 +588,7 @@ class rendering_window annotation_window output (label : GMisc.label) = GPack.vbox ~packing:window#add () in let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in + GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let _ = scrolled_window0#add !output#coerce in @@ -654,7 +654,7 @@ class theory_rendering_window rendering_window = GMisc.label ~text:"???" ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let paned = - GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in + GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let output = -- 2.39.2