diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-02-24 17:28:30 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:12:51 +0100 |
commit | 1505304e856091e10ff3511edecb9cf7c20974b2 (patch) | |
tree | 76114a50934179747878411b61b577e8945ed4fa /configure.ml | |
parent | a4f37da927bc267de505da12f5e5d626af219f90 (diff) |
Configure now fails with -with-doc yes when a doc dependency is missing.
Diffstat (limited to 'configure.ml')
-rw-r--r-- | configure.ml | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/configure.ml b/configure.ml index 1eae3bd93..435fe8626 100644 --- a/configure.ml +++ b/configure.ml @@ -959,21 +959,15 @@ let strip = 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 "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" +let _ = if !prefs.withdoc then check_doc () (** * Installation directories : bindir, libdir, mandir, docdir, etc *) @@ -1114,7 +1108,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 +1336,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; |