diff options
| author | Guillaume Melquiond | 2015-09-16 06:41:04 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-09-16 06:41:04 +0200 |
| commit | 6af9f644b64acf485c1628247f5435d09b990b79 (patch) | |
| tree | b86eedd867c0811f9b29d6a8e4dbc79ee87d9063 /kernel/nativecode.ml | |
| parent | 42ab65d7c7eed4f6696dacedceaf7c695e0d06d6 (diff) | |
Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #4268)
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions