Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[frontend]: Push to Github button should only push branch, but not creating a PR #5179

Closed
xingyaoww opened this issue Nov 21, 2024 · 4 comments · Fixed by #5181
Closed

[frontend]: Push to Github button should only push branch, but not creating a PR #5179

xingyaoww opened this issue Nov 21, 2024 · 4 comments · Fixed by #5181
Labels
enhancement New feature or request fix-me Attempt to fix this issue with OpenHands

Comments

@xingyaoww
Copy link
Collaborator

What problem or use case are you trying to solve?

After clicking the "push to github" button, the frontend will automatically send a message asking the agent to push stuff to github AND create a PR.

image

image

Describe the UX of the solution you'd like

We should have two separate buttons for the functionality of "push to remote branch", AND, "push & create a new PR" - so we don't accidentally create new PR when not intended.

Do you have thoughts on the technical implementation?

Describe alternatives you've considered

Additional context
@xingyaoww xingyaoww added the enhancement New feature or request label Nov 21, 2024
@rbren
Copy link
Collaborator

rbren commented Nov 21, 2024 •
edited
Loading

I actually disagree with this--I generally want it to open the PR. But I think adding some customizability here would be good

Edit: ah I see you're proposing a second button. That seems reasonable

@xingyaoww
Copy link
Collaborator Author

We could also do some sort of checkbox? But it might be tricky to place it near the button.. Let's ask OpenHands try to implement the two button approach and see how it'd go! @openhands-agent

@xingyaoww xingyaoww added the fix-me Attempt to fix this issue with OpenHands label Nov 21, 2024
@github-actions GitHub Actions
Copy link
Contributor

OpenHands started fixing the issue! You can monitor the progress here.

@github-actions GitHub Actions
Copy link
Contributor

A potential fix has been generated and a draft PR #5181 has been created. Please review the changes.

@openhands-agent openhands-agent mentioned this issue Nov 21, 2024
Merged
xingyaoww pushed a commit that referenced this issue Nov 25, 2024
@openhands-agent
Fix issue #5179: Rename GitHub button and show single button after PR…
4a28111 
… creation

* Rename 'Push to GitHub' button to 'Push to Branch'
* Add state to track PR creation
* Show only 'Push changes to PR' button after PR is created
* Update tests to reflect new behavior
xingyaoww added a commit that referenced this issue Nov 25, 2024
@openhands-agent @xingyaoww @neubig
Fix issue #5179: [frontend]: Push to Github button should only push b…
d267c06 
…ranch, but not creating a PR (#5181)

Co-authored-by: Xingyao Wang <[email protected]>
Co-authored-by: Xingyao Wang <[email protected]>
Co-authored-by: Graham Neubig <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request fix-me Attempt to fix this issue with OpenHands
Projects
None yet
Milestone
No milestone
2 participants
@rbren @xingyaoww