aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-11 11:11:20 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 11:21:21 +0200
commit417ac448411ce924444915da8e7e6fb81a12bc57 (patch)
treef9ab75068617f0c0a598e058da206803883d0103 /ide
parent168bb8fd5fe62beebd5e4998e903777b33654a4a (diff)
Configuration: always giving a value to configdir and datadir.
They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
Diffstat (limited to 'ide')
-rw-r--r--ide/minilib.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2c24e46f8..c9cef5639 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 ())
- @ Option.List.cons Coq_config.datadir []
+ @ [Coq_config.datadir]
let coqide_config_dirs () =
coqide_config_home ()
:: List.map coqify (Glib.get_system_config_dirs ())
- @ Option.List.cons Coq_config.configdir []
+ @ [Coq_config.configdir]
let is_prefix_of pre s =
let i = ref 0 in