From 1505304e856091e10ff3511edecb9cf7c20974b2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 24 Feb 2017 17:28:30 +0100 Subject: Configure now fails with -with-doc yes when a doc dependency is missing. --- configure.ml | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) (limited to 'configure.ml') 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; -- cgit v1.2.3