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 44e570301..749180756 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,6 +22,7 @@ val string_map : (char -> char) -> string -> string val subst_command_placeholder : string -> string -> string val home : string +val xdg_config_home : string val coqlib : string ref val coqtop_path : string ref |