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 /lib/pp_diff.ml | |
| 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 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions