diff options
| author | coqbot-app[bot] | 2020-12-30 18:31:14 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-30 18:31:14 +0000 |
| commit | 039f04c2caf7c8da380ca8d582e9edae3e6d5c06 (patch) | |
| tree | a492b93fec8f8b90a88eefc302d7d209d9cd98fe /interp/notation.ml | |
| parent | d6331216fd8f5e655ab525677ef1e1af634327b5 (diff) | |
| parent | 83bce173cf47ce216b656f47cf5fa0215375e127 (diff) | |
Merge PR #13692: Fix failing Windows CI builds.
Reviewed-by: gares
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions