diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli index 749180756..60a5eed48 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -23,6 +23,7 @@ val subst_command_placeholder : string -> string -> string val home : string val xdg_config_home : string +val xdg_config_dirs : string list val coqlib : string ref val coqtop_path : string ref |