diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-10 17:51:26 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-10 17:51:26 +0100 |
| commit | d439c01190f45de5ac493b8f55d361503e83ad03 (patch) | |
| tree | 7bc359b24f77931c6eee0f9c6d0f32fee4682e2b /configure.ml | |
| parent | a8032e02e0600c2e4b562345ce9c3baea6f0b74f (diff) | |
| parent | 49d4ca23a9d3c61df485d152de734cdc6418d89a (diff) | |
Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions