Merge pull request #2174 from whitequark/fix-github-linguist
authorwhitequark <whitequark@whitequark.org>
Fri, 19 Jun 2020 06:09:42 +0000 (06:09 +0000)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 06:09:42 +0000 (06:09 +0000)
commitbcbd44c673e07c44da735ef1d7f6eb2b6c328f98
tree3fb93d472ad6ed83cbca4596a474f60e218af5f3
parent87f45b7bd00e0a2b11c3d03161d5fc9747e21cac
parent78f39f6ebc7d613cc9cef493661648d8cda07f1c
Merge pull request #2174 from whitequark/fix-github-linguist

Fix GitHub misidentifying *.v files as Coq