diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index b696704eea..5887492ce6 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -69,9 +69,10 @@ object(self) val notebook = notebook method window = window method new_command ?command ?term () = + let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:notebook#append_page + ~packing:appendp () in notebook#goto_page (notebook#page_num frame#coerce); |