diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-30 09:39:54 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-30 09:39:54 +0200 |
commit | fd36c0451c26e44b1b7e93299d3367ad2d35fee3 (patch) | |
tree | 8b4d532931920ebf41941b2170282c63dd549c43 /tools/coqdoc | |
parent | ba3ccf80a44f0e06ee6e622a30f99de6804d005e (diff) | |
parent | a0cec18b3ac2427aaf15d2808cf021a8931a2516 (diff) |
Merge PR#356: Making management of installation directories more structured, more uniform
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5d48473d8..ef203960b 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -70,23 +70,21 @@ let normalize_filename f = let dirname = Filename.dirname f in normalize_path dirname, basename +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + (** A weaker analog of the function in Envars *) let guess_coqlib () = let file = "theories/Init/Prelude.vo" in - match Coq_config.coqlib with - | Some coqlib when Sys.file_exists (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_is_win32 then ["lib"] - else ["lib/coq"] - in - let coqlib = List.fold_left (/) prefix rpath in - if Sys.file_exists (coqlib / file) then coqlib - else prefix + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let coqlib = use_suffix prefix Coq_config.coqlibsuffix in + if Sys.file_exists (coqlib / file) then coqlib else + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) + then Coq_config.coqlib else prefix let header_trailer = ref true let header_file = ref "" |