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 /plugins | |
| parent | 396de348a4daa2ae752bed8c75a9ecacb4dcd579 (diff) | |
[configure] check that zarith dev files are available
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions