diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-03 10:31:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-03 10:31:09 +0200 |
| commit | 543aa308f4adcd6365b2390e258dde1e3f21b861 (patch) | |
| tree | 63ec1a539bf88412495b778037dd42039297282c /default.nix | |
| parent | ce848730137bd1bf1f12f88ec782c935e742d84c (diff) | |
| parent | 200fbd0cec4709bd1fb5f7a32e1c40270e343b5a (diff) | |
Merge PR #7977: allow `make check` to succeed when -prefix is given to ./configure and make install not run yet
Diffstat (limited to 'default.nix')
0 files changed, 0 insertions, 0 deletions