diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-22 16:21:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-22 16:21:07 +0200 |
| commit | 2903ee1394118106f1894798f82dc5cf3730675b (patch) | |
| tree | 76a29b8da20b51b48c6a73516a6ae9c107f57afc /configure.ml | |
| parent | 4c202177e7d1a26f3b8bc105a1ceb604f178b584 (diff) | |
| parent | 081a649157d2460c924404cd51b4ba50c23b1956 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/configure.ml b/configure.ml index 83468f8f3..ffb7c15f5 100644 --- a/configure.ml +++ b/configure.ml @@ -792,12 +792,6 @@ let md5sum = if arch = "Darwin" then "md5 -q" else "md5sum" -(** * md5sum command *) - -let md5sum = - if arch = "Darwin" then "md5 -q" else "md5sum" - - (** * Documentation : do we have latex, hevea, ... *) let check_doc () = @@ -809,6 +803,9 @@ let check_doc () = 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 |