Try fixin PR merge again

egraphs-good · Oct 17, 2024 · 4dabf6f · 4dabf6f
1 parent ee583c7
commit 4dabf6f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml
@@ -131,7 +131,7 @@ jobs:
       - run: |
           git tag "v$VERSION"
           git push --tags
-          gh pr merge --admin --delete-branch --merge
+          gh pr merge --admin --delete-branch --merge --auto
         env:
           VERSION: ${{ needs.bump.outputs.version }}
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}