diff options
| author | Gregory Malecha | 2016-02-10 10:35:01 -0800 |
|---|---|---|
| committer | Maxime Dénès | 2016-03-24 17:36:51 +0100 |
| commit | 396b598ba6984169e4215b1400989c3c67abc1aa (patch) | |
| tree | 9337d8ccd0b43805aaa08c52f9c5466879384d4b /kernel/type_errors.mli | |
| parent | 31ffc14b4b8d531777042d3ff02f34985bcec084 (diff) | |
add a .merlin target to the makefile
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions
