diff options
| author | Hugo Herbelin | 2020-07-11 20:02:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-12 10:05:25 +0200 |
| commit | 8b971260dc6381f4eaa004056c53302f291aef7e (patch) | |
| tree | c0962f6ef7966e06e324f20aab7a62162b7d88b3 /dev/ci | |
| parent | f4593ab277c12eda7e000011eeb2276716ac9a09 (diff) | |
Fixes #12682 (recursive notation printing bug with n-ary applications).
A special case for recursive n-ary applications was missing when the
head of the application was a reference.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions