aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.mli
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:03:01 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:03:01 +0000
commit6600b4e71cc82fc2a7c00e8dc1d4aa5ec1787cf7 (patch)
tree259c4924513d58738b46d15dff1007bb68f389e5 /ide/minilib.mli
parente2da4610f7e27d289ada98383c079c3c939b20c6 (diff)
CoqIdE configuration file won't pollute your home anymore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/minilib.mli')
-rw-r--r--ide/minilib.mli1
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