]> source.dussan.org Git - gitignore.git/commitdiff
projects / gitignore.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | combined (merge: 218a941 68f4c9a)
Merge pull request #3701 from JasonGross/patch-1
authorBrian Douglas <bdougie@users.noreply.github.com>
Thu, 6 May 2021 13:13:35 +0000 (06:13 -0700)
committerGitHub <noreply@github.com>
Thu, 6 May 2021 13:13:35 +0000 (06:13 -0700)
Update Coq.gitignore


Trivial merge
A collection of useful .gitignore templates: https://github.com/github/gitignore