diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 14:18:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-09 14:18:58 +0200 |
| commit | 73c2dc60ccd4d64506250a9c7476740e97ab022c (patch) | |
| tree | e3b8de9a8df55f98f6bcaf5ccf22da7b050e5a46 /pretyping/typeclasses_errors.ml | |
| parent | db0e1323d54caa3331368f6e17633475a8bb871c (diff) | |
| parent | cc2a10f1cfed35cb1ef193d23144bb10b45bcf21 (diff) | |
Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint job
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions