diff options
| author | Clément Pit-Claudel | 2019-06-14 13:03:03 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-06-14 13:03:03 -0400 |
| commit | 689cfd0674fd79a21008fa7efe17774d5efaf30f (patch) | |
| tree | 43114f6486b77e1f45c6751db7ac45a9d49eb5b8 /interp/implicit_quantifiers.ml | |
| parent | a024cf9c61b57860ce3e679be4fae427996320db (diff) | |
| parent | 821c1b27a9b9a849e5b29773bc775159aaa0a9d2 (diff) | |
Merge PR #10376: Add a comment documenting what fontsupport.py is.
Reviewed-by: cpitclaudel
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions