diff options
| author | Matej Košík | 2017-04-10 16:04:22 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-04-10 16:04:22 +0200 |
| commit | cec95b3e62e973af5a6aa1cb571c3c4654c3005e (patch) | |
| tree | 0994065d774a9bf8faf9280381aba4a6805d9cce /kernel/type_errors.ml | |
| parent | 69d0152e00c2a3c7341bef36dcb110a2c4263ccf (diff) | |
Revert "comment: typo"
This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions