diff options
Diffstat (limited to 'ide/configwin_ihm.mli')
| -rw-r--r-- | ide/configwin_ihm.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli index c867ad9127..94a3f12b39 100644 --- a/ide/configwin_ihm.mli +++ b/ide/configwin_ihm.mli @@ -60,6 +60,7 @@ val edit : ?with_apply:bool -> ?apply:(unit -> unit) -> string -> + ?parent:GWindow.window -> ?width:int -> ?height:int -> configuration_structure list -> |