diff options
| author | Clément Pit-Claudel | 2020-05-12 23:42:43 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-12 23:42:43 -0400 |
| commit | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (patch) | |
| tree | a97a373e1fe45a7b7fbd18fd36ca9d495470e4f4 /checker/check.ml | |
| parent | 4a5944448e31022593df7d6e7e0318cfea92ea98 (diff) | |
| parent | e3e889c01db5382d761d2455370ddc8a793c8e2d (diff) | |
Merge PR #12309: Remove documentation of -compile, which was removed in #8690.
Diffstat (limited to 'checker/check.ml')
0 files changed, 0 insertions, 0 deletions