diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:27:35 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:27:35 +0100 |
commit | 2069c0aec44a50031e33bcb9f7d86c1535ef6b84 (patch) | |
tree | f1fb49a4d56af2579b7c9f602e5766e6f7e6daea /dev/tools/check-eof-newline.sh | |
parent | ff947d85f8b8921e401b693e47c52504c71f9c4c (diff) | |
parent | 296fd47808c5642903a81bf6a87bf291ae15abfd (diff) |
Merge PR #6941: [toplevel] Respect COQ_COLORS environment variable
Diffstat (limited to 'dev/tools/check-eof-newline.sh')
0 files changed, 0 insertions, 0 deletions