aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/minilib.ml')
-rw-r--r--ide/minilib.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 825fc58cc..6a960e266 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -38,3 +38,18 @@ let log ?(level = `DEBUG) msg =
try Printf.eprintf "[%s] %s\n%!" prefix msg
with _ -> ()
end
+
+let coqify d = Filename.concat d "coq"
+
+let coqide_config_home () =
+ coqify (Glib.get_user_config_dir ())
+
+let coqide_data_dirs () =
+ coqify (Glib.get_user_data_dir ())
+ :: List.map coqify (Glib.get_system_data_dirs ())
+ @ Option.List.cons Coq_config.datadir []
+
+let coqide_config_dirs () =
+ coqide_config_home ()
+ :: List.map coqify (Glib.get_system_config_dirs ())
+ @ Option.List.cons Coq_config.configdir []