diff options
| author | Maxime Dénès | 2017-12-05 09:56:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 09:56:49 +0100 |
| commit | 2ae7674c6788742c021988ac02caabceec958957 (patch) | |
| tree | 8f8c17a32a4a77ace1eac05760847c8c12d35670 /API | |
| parent | 14c041012bd375cae018f83d107c836fca3d1f01 (diff) | |
| parent | 6cb9ab00a62b87587b00147d4abd82e684220b03 (diff) | |
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions