diff options
author | Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
commit | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch) | |
tree | 142a99bc1cd3beef403f1942908de090f70c5e07 /ide/command_windows.ml | |
parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) |
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'ide/command_windows.ml')
-rw-r--r-- | ide/command_windows.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 768d125c..937098b7 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 9189 2006-09-29 12:39:24Z notin $ *) +(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *) class command_window () = let window = GWindow.window @@ -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); |