From 417ac448411ce924444915da8e7e6fb81a12bc57 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Nov 2016 11:11:20 +0100
Subject: 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.
---
 ide/minilib.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2c24e46f8f..c9cef5639b 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
-- 
cgit v1.2.3


From 5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Nov 2016 04:01:29 +0100
Subject: Relying on computation done in Envars to discover the installation
 directories.

This allows to share the test for possible relocalisation done in envars.ml.
---
 ide/ideutils.ml    | 2 +-
 ide/minilib.ml     | 4 ++--
 ide/preferences.ml | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'ide')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a08ab07b5f..8a0e507c0b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -422,7 +422,7 @@ let browse prerr url =
 let doc_url () =
   if doc_url#get = use_default_doc_url || doc_url#get = ""
   then
-    let addr = List.fold_left Filename.concat (Coq_config.docdir)
+    let addr = List.fold_left Filename.concat (Envars.docdir ())
       ["html";"refman";"index.html"]
     in
     if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
diff --git a/ide/minilib.ml b/ide/minilib.ml
index c9cef5639b..2b278fac69 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
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 9fe9c6337d..d97e499276 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () =
   in
   let doc_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]);
+      "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]);
       Coq_config.wwwrefman;
       use_default_doc_url
     ] in
@@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () =
       doc_url#get in
   let library_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]);
+      "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]);
       Coq_config.wwwstdlib
     ] in
     combo
-- 
cgit v1.2.3