diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli index 53d6c87c2..7df949cbb 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -21,11 +21,11 @@ val string_map : (char -> char) -> string -> string val subst_command_placeholder : string -> string -> string -val home : string -val xdg_config_home : string -val xdg_config_dirs : string list -val xdg_data_home : string -val xdg_data_dirs : string list +val home : unit -> string +val xdg_config_home : unit -> string +val xdg_config_dirs : unit -> string list +val xdg_data_home : unit -> string +val xdg_data_dirs : unit -> string list val coqtop_path : string ref |