aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ide/wg_Notebook.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli
index 85ecdf6cdd..9447b21c0b 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/wg_Notebook.mli
@@ -28,11 +28,10 @@ val create :
('a -> GObj.widget option * GObj.widget option * GObj.widget) ->
('a -> unit) ->
?enable_popup:bool ->
- ?homogeneous_tabs:bool ->
+ ?group_name:string ->
?scrollable:bool ->
?show_border:bool ->
?show_tabs:bool ->
- ?tab_border:int ->
?tab_pos:Gtk.Tags.position ->
?border_width:int ->
?width:int ->