diff options
| author | Emilio Jesus Gallego Arias | 2019-12-07 18:28:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-07 18:33:43 +0100 |
| commit | 55e54479837cc70a5c070220a0bf32d0bbf55212 (patch) | |
| tree | bf3980d0ae636b9a3500146c2e5e3032c32cf0fc /_CoqProject | |
| parent | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (diff) | |
[configure] [dune] Fix configure under Dune in 32bit builds.
`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.
Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions