diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-09 13:55:54 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-25 13:41:52 +0200 |
commit | 54b9591a82889e3cdb31325e22c5af3e0e69e3df (patch) | |
tree | ca98f0c6b5c61f0ce8cded65edadcf634003ee02 /interp/genintern.ml | |
parent | f1598b00219a951e94036cb7f48a8fe1309025f1 (diff) |
Add linter.
Diffstat (limited to 'interp/genintern.ml')
0 files changed, 0 insertions, 0 deletions