diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-27 14:36:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-27 14:36:30 +0200 |
| commit | 53fb4203b80da48e2ac9b06803c57e81df702a0a (patch) | |
| tree | 0dc2a8efe8012190fcfcda50faf65365e30a3bad /tools | |
| parent | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (diff) | |
| parent | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (diff) | |
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.univ_print
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions