diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-05 22:48:45 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-05 22:48:45 +0200 |
| commit | cebab877a73d46628a85fa5d5b0ae1f1bb00d285 (patch) | |
| tree | 53cccf63c28f773e40566eea75b233465d425f97 /checker/typeops.ml | |
| parent | c9c9be2c3eb451ac5bcc1bc08f98b3176f29c84d (diff) | |
| parent | 54cf593ec1c47ecd5a875714e8e0857707c72901 (diff) | |
Merge PR#724: Move README.ci to markdown
Diffstat (limited to 'checker/typeops.ml')
0 files changed, 0 insertions, 0 deletions