-
Notifications
You must be signed in to change notification settings - Fork 4.2k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix issue #5179: [frontend]: Push to Github button should only push branch, but not creating a PR #5181
base: main
Are you sure you want to change the base?
Conversation
…ranch, but not creating a PR
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@openhands-agent you should do npm run lint:fix
to fix frontend linting.
…ld only push branch, but not creating a PR
New OpenHands update |
The workflow to fix this issue encountered an error. Please check the workflow logs for more information. |
The workflow to fix this issue encountered an error. Please check the workflow logs for more information. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we get a screenshot of the resulting design? I'm a little bit worried about the design becoming noisy.
@neubig edited the PR description to include a screenshot |
Thanks! @rbren , wdyt about this design? For me personally I think it might be nice if we could put the buttons side-by-side to save screen space? |
@openhands-agent Can you put these two button side to side? |
…ld only push branch, but not creating a PR
New OpenHands update |
The workflow to fix this issue encountered an error. Please check the workflow logs for more information. |
@openhands-agent please display the "Push to Github" and "Push & Create PR" button side-by-side |
This pull request fixes #5179.
The PR has successfully resolved the original issue by implementing the requested split functionality for GitHub interactions. Specifically:
The original single "Push to GitHub" button that automatically created PRs has been separated into two distinct buttons:
The implementation includes proper test coverage to verify:
The changes maintain backward compatibility while adding the requested granular control over GitHub operations.
This solution directly addresses the original problem by preventing unintended PR creation while still maintaining the ability to create PRs when desired. The clear separation of concerns through distinct buttons provides a better user experience aligned with the requested solution.
A reviewer can verify that:
Automatic fix generated by OpenHands 🙌
It looks something like this:
To run this PR locally, use the following command: