diff options
| author | Enrico Tassi | 2020-11-18 11:57:50 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-18 17:52:05 +0100 |
| commit | c3ea4b4c9ace031d70e55326675b63ddce8d9b3c (patch) | |
| tree | 4fe3901165d49db6d7c109f4fb87d6f3fde30c01 | |
| parent | 396de348a4daa2ae752bed8c75a9ecacb4dcd579 (diff) | |
[configure] check that zarith dev files are available
| -rw-r--r-- | configure.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index 7fd1acb53e..6a4b1f9a75 100644 --- a/configure.ml +++ b/configure.ml @@ -692,10 +692,13 @@ let operating_system = let check_for_zarith () = let zarith,_ = tryrun camlexec.find ["query";"zarith"] in + let zarith_cmai base = Sys.file_exists (base / "z.cmi") && Sys.file_exists (base / "zarith.cma") in let zarith_version, _ = run camlexec.find ["query"; "zarith"; "-format"; "%v"] in match zarith with | "" -> die "Zarith library not installed, required" + | _ when not (zarith_cmai zarith) -> + die "Zarith library installed but no development files found (try installing the -dev package)" | _ -> let zarith_version_int = List.map int_of_string (numeric_prefix_list zarith_version) in if zarith_version_int >= [1;10;0] then |
