push branch manually before creating PR

egraphs-good · Apr 27, 2024 · 8520903 · 8520903
1 parent 980f72d
commit 8520903
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml
@@ -37,7 +37,8 @@ jobs:
           VERSION=$(python increment_version.py $TYPE)
           git checkout -b "release-$VERSION"
           git commit -am "Version $VERSION"
-          gh pr create --fill --head release-$VERSION --base main
+          git push -u origin HEAD
+          gh pr create --fill
           echo "version=$VERSION" >> "$GITHUB_OUTPUT"
         id: bump
         env: