diff options
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/configure.ml b/configure.ml index 1eae3bd93..4726831e4 100644 --- a/configure.ml +++ b/configure.ml @@ -957,23 +957,18 @@ 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 = - ceprintf "%s was not found; documentation will not be available" s; - raise Not_found + die (sprintf "A documentation build was requested, but %s was not found." s); in - try - if not !prefs.withdoc then raise Not_found; - 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"; - true - with Not_found -> false - -let withdoc = check_doc () + 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 () (** * Installation directories : bindir, libdir, mandir, docdir, etc *) @@ -1114,7 +1109,7 @@ let print_summary () = pr " Mac OS integration is on\n"; pr " CoqIde : %s\n" coqide; pr " Documentation : %s\n" - (if withdoc then "All" else "None"); + (if !prefs.withdoc then "All" else "None"); pr " Web browser : %s\n" browser; pr " Coq web site : %s\n" !prefs.coqwebsite; pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; @@ -1342,7 +1337,7 @@ let write_makefile f = pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; - pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); + pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else ""); close_out o; |