aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-02-24 17:28:30 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 15:12:51 +0100
commit1505304e856091e10ff3511edecb9cf7c20974b2 (patch)
tree76114a50934179747878411b61b577e8945ed4fa /configure.ml
parenta4f37da927bc267de505da12f5e5d626af219f90 (diff)
Configure now fails with -with-doc yes when a doc dependency is missing.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml24
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;