Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CI: Checkout out PR HEAD commit instead of merge commit
The `checkout` action's default behavior is to create a merge commit during CI that merges the changes from the PR branch, but this will cause `cryptol --version` to print the SHA of the merge commit rather than the most recent HEAD commit, which is what users and developers actually care about. This commit follows the advice from https://github.com/actions/checkout/tree/96f53100ba2a5449eb71d2e6604bbcd94b9449b5#checkout-pull-request-head-commit-instead-of-merge-commit to change `checkout`'s behavior to use the HEAD commit instead.
- Loading branch information