diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index f1a2fa4f2a..dcae3e38a5 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -93,9 +93,9 @@ object(self) combo, entry, ok_b in let r_bin = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(vbox#pack ~fill:true ~expand:true) () in + ~vpolicy:`AUTOMATIC + ~hpolicy:`AUTOMATIC + ~packing:(vbox#pack ~fill:true ~expand:true) () in let result = Wg_MessageView.message_view () in router#register_route route_id result; r_bin#add_with_viewport (result :> GObj.widget); |