diff options
| author | Enrico Tassi | 2015-07-01 11:25:47 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-01 11:25:55 +0200 |
| commit | 0917ce7cf48cadacc6fca48ba18b395740cccbe2 (patch) | |
| tree | 883b3c7e087e8791fbe8cf5c2bbf2b2676f34013 /kernel/cbytecodes.ml | |
| parent | 72f128af5a00e5509239e46b395c9cd10e53b36a (diff) | |
Notation: use same level for "@" in constr: and pattern: (Close: #4272)
A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).
Thanks Georges for debugging that.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions
