diff options
| author | Hugo Herbelin | 2018-05-13 22:28:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-13 22:46:17 +0200 |
| commit | ea271504e92ec30991e9767e0fbe2e536bc3417e (patch) | |
| tree | a3a55b0bf0c4a9c4befd6b31520b0721613bd649 /dev/ci | |
| parent | 8256236dd59c753da186173f4d227565903f123a (diff) | |
Fixing a bug in printing the body of a located notation.
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions