aboutsummaryrefslogtreecommitdiffstats
path: root/.gitattributes
Commit message (Collapse)AuthorAgeFilesLines
* Make GIT_REV logic work in release tarballsDaniel Gröber2022-05-251-0/+1
| | | | | | | | | | | | Currently GIT_REV doesn't get set properly when building a release tarball. To fix this we arrange for .gitcommit to contain the (short) commit hash in tarballs generated with git-archive(1) using export-subst in gitattributes. This way the correct commit hash is (reproducibly) included in the release tarballs while not burdening the maintainers with updating it in the git repo. Please note this even works on Github and similar forges as they use git-archive for generating tarballs so this works out quite nicely.
* Fix GitHub misidentifying *.v files as Coq.whitequark2020-06-191-0/+1