diff options
| author | Nick Lewycky | 2018-09-22 17:29:16 -0700 |
|---|---|---|
| committer | Nick Lewycky | 2018-09-22 17:29:32 -0700 |
| commit | e186109404b665d79bf441f8d1ccee39cc76b165 (patch) | |
| tree | 4c93803554ac6cc9b2da26875650688c41874fc5 /kernel/type_errors.ml | |
| parent | 4d1de421c2df95503e4643f41903d214e0c2fb19 (diff) | |
Fix typo in comment.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions