diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-02-10 15:52:24 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:12:51 +0100 |
| commit | 4aaf28cc905bebf757b02ad911a6eed78714cac7 (patch) | |
| tree | 91322ece8b35fc82247938d8a5dc0e70cd22597b /configure.ml | |
| parent | 1505304e856091e10ff3511edecb9cf7c20974b2 (diff) | |
Integration of a sphinx-based documentation generator.
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/configure.ml b/configure.ml index 435fe8626..4726831e4 100644 --- a/configure.ml +++ b/configure.ml @@ -957,15 +957,16 @@ let strip = (** * Documentation : do we have latex, hevea, ... *) +let check_sphinx_deps () = + ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"]) + let check_doc () = let err s = die (sprintf "A documentation build was requested, but %s was not found." s); in - if not (program_in_path "latex") then err "latex"; - if not (program_in_path "hevea") then err "hevea"; - if not (program_in_path "hacha") then err "hacha"; - if not (program_in_path "fig2dev") then err "fig2dev"; - if not (program_in_path "convert") then err "convert" + if not (program_in_path "python3") then err "python3"; + if not (program_in_path "sphinx-build") then err "sphinx-build"; + check_sphinx_deps () let _ = if !prefs.withdoc then check_doc () |