diff options
| author | Hugo Herbelin | 2018-10-15 15:50:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 8f7c82b8a67a3c94073e55289996f02285c04914 (patch) | |
| tree | e219713f3408297c18da63186f40bb0b8ab0360e /dev/ci | |
| parent | e2c4d3ad72b85f1fb1ea1a7c42aff0831eff3c30 (diff) | |
Printing priority to most recent notation in case of non-open scopes with delim.
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions