diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 1da8b3157..48c2a6410 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -29,6 +29,8 @@ object method connect : 'a preference_signals method get : 'a method set : 'a -> unit + method reset : unit -> unit + method default : 'a end val cmd_coqtop : string option preference |