Test if PR is merged

echoix · Sep 28, 2024 · 16233db · 16233db
1 parent 0b88763
commit 16233db
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/.github/workflows/milestones.yml b/.github/workflows/milestones.yml
@@ -11,6 +11,8 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event.pull_request.merged || true
     steps:
+      - run: echo "pull_request is merged"
+        if: github.event.pull_request.merged
       - name: Dump GitHub context
         env:
           GITHUB_CONTEXT: ${{ toJson(github) }}