diff options
| author | Emilio Jesus Gallego Arias | 2019-02-17 01:03:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-20 13:34:15 +0100 |
| commit | 565a30614c6df16466f66cac1e517f9202612709 (patch) | |
| tree | 4deae898a650f25eb0288f7bfc1df0b151e9c9d2 /tools | |
| parent | 756b978dfee0e0c103a5244af21115233ad96358 (diff) | |
[azure] [ci] Build on Windows using Dune.
We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.
In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.
While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 0d3fb77551..5dd6cc6c83 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -79,14 +79,17 @@ let use_suffix prefix suffix = (** A weaker analog of the function in Envars *) +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + let guess_coqlib () = + getenv_else "COQLIB" (fun () -> let file = "theories/Init/Prelude.vo" in 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 + then Coq_config.coqlib else prefix) let header_trailer = ref true let header_file = ref "" |
