aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/minilib.ml')
-rw-r--r--ide/minilib.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml
index c9cef5639..2b278fac6 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -54,12 +54,12 @@ let coqide_config_home () =
let coqide_data_dirs () =
coqify (Glib.get_user_data_dir ())
:: List.map coqify (Glib.get_system_data_dirs ())
- @ [Coq_config.datadir]
+ @ [Envars.datadir ()]
let coqide_config_dirs () =
coqide_config_home ()
:: List.map coqify (Glib.get_system_config_dirs ())
- @ [Coq_config.configdir]
+ @ [Envars.configdir ()]
let is_prefix_of pre s =
let i = ref 0 in