diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 23:56:30 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-16 16:27:00 +0100 |
commit | 0300aa85f3ba8cc7cdd38f719628dc0a28170c84 (patch) | |
tree | fc110af8c2aea6d5c2c73bfd8c63bb50d1084c57 /pretyping/tacred.mli | |
parent | c671d86beecb4e31ad5c7752f7e4fb570823e837 (diff) |
Simplify logic and streamline lint-repository.sh
We inline should-check-whitespace.sh in check-eof-newline.sh
simplifying the find invocation.
Diffstat (limited to 'pretyping/tacred.mli')
0 files changed, 0 insertions, 0 deletions