diff options
Diffstat (limited to 'ide/undo_lablgtk_ge212.mli')
| -rw-r--r-- | ide/undo_lablgtk_ge212.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli index 4488b5e9..7b7026bd 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo_lablgtk_ge212.mli @@ -19,7 +19,7 @@ object method clear_undo : unit end -val undoable_view : +val undoable_view : ?buffer:GText.buffer -> ?editable:bool -> ?cursor_visible:bool -> |