diff options
| author | Emilio Jesus Gallego Arias | 2018-07-03 10:31:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-03 10:31:09 +0200 |
| commit | 543aa308f4adcd6365b2390e258dde1e3f21b861 (patch) | |
| tree | 63ec1a539bf88412495b778037dd42039297282c /tools/TimeFileMaker.py | |
| 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 'tools/TimeFileMaker.py')
0 files changed, 0 insertions, 0 deletions