Merge pull request #274507 from tweag/by-name-cancel

  # Using pull_request_target instead of pull_request avoids having to approve first time contributors

  pull_request_target

# The tool doesn't need any permissions, it only outputs success or not based on the checkout

permissions: {}

permissions:

  # We need this permission to cancel the workflow run if there's a merge conflict

  actions: write

jobs:

  check:

          if [[ "$mergeable" == "true" ]]; then

            echo "The PR can be merged, checking the merge commit $mergedSha"

          else

            echo "The PR cannot be merged, it has a merge conflict"

            echo "The PR cannot be merged, it has a merge conflict, cancelling the workflow.."

            gh api \

              --method POST \

              -H "Accept: application/vnd.github+json" \

              -H "X-GitHub-Api-Version: 2022-11-28" \

              /repos/"$GITHUB_REPOSITORY"/actions/runs/"$GITHUB_RUN_ID"/cancel

            sleep 60

            # If it's still not canceled after a minute, something probably went wrong, just exit

            exit 1

          fi

          echo "mergedSha=$mergedSha" >> "$GITHUB_ENV"