Open naftulikay opened 1 year ago
In a pull request, pr #3, c172060
:
github.event_type=pull_request
github.base_ref=main
github.head_ref=feature/auditable
github.ref=refs/pull/3/merge
github.ref_name=3/merge
github.sha=c17206090b446fd7e4168fe8afebb591badd8572
On push of cd08f27
to main:
github.event_type=push
github.base_ref=
github.head_ref=
github.ref=refs/heads/main
github.ref_name=main
github.sha=cd08f270c2aa0a9932c690ffa5a8f413028409f4
Full GitHub Event from PR:
github.event.id
is 5
, which seems to correlate with PR number.git checkout main
and then figure out what the commit ID is, can't find it in the event.Full GitHub Event from Push:
For benchmarking in GitHub Actions:
if: ${{ github.event_name == 'pull_request' }}
${{ github.base_ref }}
cargo bench -- --save-baseline main@${{ github.base_ref }}
if: ${{ github.event_name != 'pull_request' }}
main~1
cargo bench -- --save-baseline main@${{ commit_id }}
By using these names, it'll be easier when viewing reports to see what given profiles cover in the form of
main@${COMMIT_SHA}
.