diff options
| author | Emilio Jesus Gallego Arias | 2020-07-21 15:17:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-21 15:17:32 +0200 |
| commit | 8f4d7ddf4c3736a190b3e073fadb844c017628d3 (patch) | |
| tree | 54b6ff9f33a174f60f3dc431ac6c2a677ac3395a /dev | |
| parent | f44202e28f38aa900801b0c90514690b6a401bed (diff) | |
| parent | fff15259300b42d83e0d135aa3abc10f274f719d (diff) | |
Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions