diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 00:02:32 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 00:02:32 +0100 |
| commit | 7576ffd4eb196d5d5a15f6cacb2ba5cba00576ef (patch) | |
| tree | c029a02199a84e501c55be959e82e5d5c4f99677 /configure.ml | |
| parent | e32f176cf8f8637aee98c5335af7e4b3e375aed3 (diff) | |
| parent | 17e800a8e0501c242d954a98dde12f28f01f40c0 (diff) | |
Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards compatible change.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions