diff options
Diffstat (limited to 'ide/typed_notebook.ml')
| -rw-r--r-- | ide/typed_notebook.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml index edc5c599c..39e8155d3 100644 --- a/ide/typed_notebook.ml +++ b/ide/typed_notebook.ml @@ -12,7 +12,7 @@ class ['a] typed_notebook default_build nb = object(self) inherit GPack.notebook nb as super val mutable term_list = [] - + method append_term ?(build=default_build) (term:'a) = let tab_label,menu_label,page = build term in (* XXX - Temporary hack to compile with archaic lablgtk *) |