aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
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