diff options
| author | Hugo Herbelin | 2020-07-15 13:07:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-15 18:08:00 +0200 |
| commit | fff15259300b42d83e0d135aa3abc10f274f719d (patch) | |
| tree | acd127e09eae048032b38db3bfe2e960c566c326 /dev/ci | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
Fix bug #12691 (an only parsing notation induces a generic printing format).
This is to anticipate further not-only-parsing uses of the notation.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions