diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 41 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 25 |
2 files changed, 35 insertions, 31 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index a412e68652..6b8a3f5e78 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -49,21 +49,40 @@ type glob_source_t = let glob_source = ref DotGlob +(*s Manipulations of paths and path aliases *) + +let normalize_path p = + (* We use the Unix subsystem to normalize a physical path (relative + or absolute) and get rid of symbolic links, relative links (like + ./ or ../ in the middle of the path; it's tricky but it + works... *) + (* Rq: Sys.getcwd () returns paths without '/' at the end *) + let orig = Sys.getcwd () in + Sys.chdir p; + let res = Sys.getcwd () in + Sys.chdir orig; + res + +let normalize_filename f = + let basename = Filename.basename f in + let dirname = Filename.dirname f in + normalize_path dirname, basename + (** A weaker analog of the function in Envars *) let guess_coqlib () = let file = "states/initial.coq" in - if Sys.file_exists (Filename.concat Coq_config.coqlib file) - then Coq_config.coqlib - else - let coqbin = Filename.dirname Sys.executable_name in - let prefix = Filename.dirname coqbin in - let rpath = if Coq_config.local then [] else - (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in - let coqlib = List.fold_left Filename.concat prefix rpath in - if Sys.file_exists (Filename.concat coqlib file) then coqlib - else - Coq_config.coqlib + match Coq_config.coqlib with + | Some coqlib when Sys.file_exists (Filename.concat coqlib file) -> + coqlib + | Some _ | None -> + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let rpath = if Coq_config.local then [] else + (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in + let coqlib = List.fold_left Filename.concat prefix rpath in + if Sys.file_exists (Filename.concat coqlib file) then coqlib + else prefix let header_trailer = ref true let header_file = ref "" diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 98204a856d..7dc2c3bf28 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -106,25 +106,6 @@ let check_if_file_exists f = end -(*s Manipulations of paths and path aliases *) - -let normalize_path p = - (* We use the Unix subsystem to normalize a physical path (relative - or absolute) and get rid of symbolic links, relative links (like - ./ or ../ in the middle of the path; it's tricky but it - works... *) - (* Rq: Sys.getcwd () returns paths without '/' at the end *) - let orig = Sys.getcwd () in - Sys.chdir p; - let res = Sys.getcwd () in - Sys.chdir orig; - res - -let normalize_filename f = - let basename = Filename.basename f in - let dirname = Filename.dirname f in - normalize_path dirname, basename - (* [paths] maps a physical path to a name *) let paths = ref [] @@ -354,7 +335,11 @@ let parse () = | ("--coqlib" | "-coqlib") :: [] -> usage () | ("--boot" | "-boot") :: rem -> - Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem + Cdglobals.coqlib_path := normalize_path ( + Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + ); parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> |