aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-12 04:01:29 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 12:12:57 +0200
commit5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 (patch)
treeaec2a11ab2b73620eb02b49c412f645f7241f868 /ide/minilib.ml
parent66b98ecd41bac232bbee19a9b3484feefd71df3c (diff)
Relying on computation done in Envars to discover the installation directories.
This allows to share the test for possible relocalisation done in envars.ml.
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