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.

1 files changed, 14 insertions, 16 deletions

diff --git a/configure.ml b/configure.ml
index 9902946e3..128751ea3 100644
--- a/configure.ml
+++ b/configure.ml
@@ -891,35 +891,33 @@ let relativize = function
   | Absolute path -> Relative (String.sub path 1 (String.length path - 1))
 
 let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) =
-  let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in
   let dir = match !uservalue, !Prefs.prefix with
     | Some d, _ -> d
     | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout)
     | _ ->
+      let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in
       let () = printf "Where should I install %s [%s]? " msg dflt in
       let line = read_line () in
       if line = "" then dflt else line
-  in (var,msg,dir,dir<>dflt)
+  in (var,msg,dir)
 
 let do_one_noinst (var,msg,_,_,_) =
-  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true)
-  else (var,msg,coqtop^"/doc",false)
+  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide")
+  else (var,msg,coqtop^"/doc")
 
 let install_dirs =
   let f = if !Prefs.local then do_one_noinst else do_one_instdir in
   List.map f install
 
-let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs
+let select var = List.find (fun (v,_,_) -> v=var) install_dirs
 
-let coqlib = let (_,_,d,_) = select "COQLIBINSTALL" in d
+let coqlib = let (_,_,d) = select "COQLIBINSTALL" in d
 
-let docdir = let (_,_,d,_) = select "DOCDIR" in d
+let docdir = let (_,_,d) = select "DOCDIR" in d
 
-let configdir =
-  let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None
+let configdir = let (_,_,d) = select "CONFIGDIR" in d
 
-let datadir =
-  let (_,_,d,b) = select "DATADIR" in if b then Some d else None
+let datadir = let (_,_,d) = select "DATADIR" in d
 
 
 (** * OCaml runtime flags *)
@@ -986,7 +984,7 @@ let print_summary () =
   else
     (pr "  Paths for true installation:\n";
      List.iter
-       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
+       (fun (_,msg,dir) -> pr "  - %s will be copied in %s\n" msg dir)
        install_dirs);
   pr "\n";
   pr "If anything is wrong above, please restart './configure'.\n\n";
@@ -1033,8 +1031,8 @@ let write_configml f =
   pr_b "local" !Prefs.local;
   pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
   pr_o "coqlib" (if !Prefs.local then None else Some coqlib);
-  pr_o "configdir" configdir;
-  pr_o "datadir" datadir;
+  pr_s "configdir" configdir;
+  pr_s "datadir" datadir;
   pr_s "docdir" docdir;
   pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
@@ -1119,8 +1117,8 @@ let write_makefile f =
   pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags);
   pr "%s\n\n" !build_loadpath;
   pr "# Paths for true installation\n";
-  List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
-  List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
+  List.iter (fun (v,msg,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
+  List.iter (fun (v,_,dir) -> pr "%s=%S\n" v dir) install_dirs;
   pr "\n# Coq version\n";
   pr "VERSION=%s\n" coq_version;
   pr "VERSION4MACOS=%s\n\n" coq_macos_version;