From 99f3f1db6ba7e9d65e5c764345d8a3f6a73c66ab Mon Sep 17 00:00:00 2001 From: Rain Date: Sun, 1 Oct 2023 21:09:01 -0700 Subject: [PATCH] [ci] check out merge commit rather than PR tip I've decided checking out a merge is better. --- .github/workflows/ci.yml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index efd5404..baa0c97 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,10 +15,6 @@ jobs: RUSTFLAGS: -D warnings steps: - uses: actions/checkout@ee0669bd1cc54295c223e0bb666b733df41de1c5 # v2 - with: - # By default actions/checkout checks out a merge commit. Check out the PR head instead. - # https://github.com/actions/checkout#checkout-pull-request-head-commit-instead-of-merge-commit - ref: ${{ github.event.pull_request.head.sha }} - uses: actions-rs/toolchain@16499b5e05bf2e26879000db0c1d13f7e13fa3af # v1 with: toolchain: stable