diff options
| author | Jim Fehrle | 2018-10-04 16:56:08 -0700 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-10 19:34:04 +0200 |
| commit | 3a0a9c27dad3e3177416d703b996c699c7a0542c (patch) | |
| tree | 3cb27a8e9236499fc4ae15f306032767887c51fb /kernel/type_errors.ml | |
| parent | 040ad198e38776bb9f398329243b2fe41434f2d5 (diff) | |
Fix names for 2 entries in Flags, Options, Tables index.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions