diff options
| author | coqbot-app[bot] | 2020-09-28 16:18:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-28 16:18:52 +0000 |
| commit | 982c28216f3eb49abfd6b97c69b8fc116c813117 (patch) | |
| tree | 47edf047d93d4ead9d52afc795c812c34063a503 /dev/include_dune | |
| parent | bd24f72a06343b375ad20aaa5b7296c2ad904a5c (diff) | |
| parent | a0090dc6930c1f0c60ca6144d1551019ecbcc837 (diff) | |
Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lonely notation at printing time.
Reviewed-by: ejgallego
Ack-by: maximedenes
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions