summaryrefslogtreecommitdiff
path: root/tools/coqdoc/cdglobals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/cdglobals.ml')
-rw-r--r--tools/coqdoc/cdglobals.ml34
1 files changed, 17 insertions, 17 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5d48473d..0d3fb775 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
@@ -70,23 +72,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 ""