diff options
| author | Pierre Letouzey | 2016-06-08 15:13:13 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-08 15:15:06 +0200 |
| commit | f6ce65b4d49f0a3a3af7e0e7811934136f59943c (patch) | |
| tree | d7b48be2926891e20890eed4384dd42e1c110bb1 /kernel/nativecode.mli | |
| parent | d060577f274658dd8189fceb92316b3cd37417b9 (diff) | |
remove grammar/grammar.mllib
grammar.cma is built by Makefile.build in a specific, hardcoded way.
Let's remove this old .mllib file to avoid potential confusions in
the future.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions