projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54845b5) | patch
Use proper commit hash for PRs (#6485)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 4 May 2021 17:06:35 +0000 (19:06 +0200)
committerGitHub <noreply@github.com>
Tue, 4 May 2021 17:06:35 +0000 (17:06 +0000)
commit4f265b2c81c4cb858942f6e1e51ce8abdd01345b
tree11059b0ebf4fd5ab9e0191af70809bd817e8a1bftree
parent54845b5aba4e759c5a7db89226b9e824c7ef1d6ccommit | diff
Use proper commit hash for PRs (#6485)

For PRs, the automatically generated documentation is stored under the current master commit hash instead of the hash of the latest commit on the PR. This PR fixes this issue by exporting the commit hash (much like the name of the PR or branch).
.github/workflows/docs_update.yml diff | blob | history