diff options
| author | Emilio Jesus Gallego Arias | 2019-01-28 13:33:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-28 14:31:33 +0100 |
| commit | 9f20e5a063cd268fdd91a3b827efac1f6f4cb4f4 (patch) | |
| tree | 5723956b18ada828189544ff62dd9d79c5ee5eeb /kernel/type_errors.mli | |
| parent | 5aa4b87d4ed71a22a696ae73af77ced8f5c6da47 (diff) | |
[doc] Remove emacs mentions from INSTALL
Fixes #9418
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions