diff options
| -rw-r--r-- | config/coq_config.mli | 4 | ||||
| -rw-r--r-- | configure.ml | 30 | ||||
| -rw-r--r-- | ide/minilib.ml | 4 | ||||
| -rw-r--r-- | lib/envars.ml | 4 |
4 files changed, 19 insertions, 23 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index c171bd355..59c96f73d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -9,8 +9,8 @@ val local : bool (* local use (no installation) *) val coqlib : string option (* where the std library is installed *) -val configdir : string option (* where configuration files are installed *) -val datadir : string option (* where extra data files are installed *) +val configdir : string (* where configuration files are installed *) +val datadir : string (* where extra data files are installed *) val docdir : string (* where the doc is installed *) val ocaml : string (* names of ocaml binaries *) 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; 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 diff --git a/lib/envars.ml b/lib/envars.ml index 0974368f6..989a18db9 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -23,8 +23,6 @@ let ( / ) a b = let coqify d = d / "coq" -let opt2list = function None -> [] | Some x -> [x] - let home ~warn = getenv_else "HOME" (fun () -> try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> @@ -189,7 +187,7 @@ let xdg_data_dirs warn = | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"] | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] in - xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir + xdg_data_home warn :: sys_dirs @ [Coq_config.datadir] let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) |