diff options
| author | Clément Pit-Claudel | 2020-12-11 09:11:27 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-12-11 09:11:27 -0500 |
| commit | c8d2248cbbe2c713605e0c61d7342fad948072da (patch) | |
| tree | f847bb885217a724d4b44762bda72ed293447b76 /interp/notation_ops.ml | |
| parent | edc599b876949b8a093446cebd7fd3964f9a7c3f (diff) | |
| parent | 1605ae821f151f1e4b4edab9a0dded02cb91eebf (diff) | |
Merge PR #13611: Clarify changelog categories.
Reviewed-by: cpitclaudel
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions