github/OpenHands
1
0
Fork 0
mirror of https://github.com/OpenHands/OpenHands.git synced 2025-12-26 05:48:36 +08:00
Code Issues Packages Projects Releases Wiki Activity

Update github microagent for draft PRs and not creating new branches/PRs (#5986)

Browse Source 
Co-authored-by: Xingyao Wang <xingyao@all-hands.dev>
This commit is contained in:
Robert Brennan 2025-01-03 09:29:17 -05:00 committed by GitHub
parent 23df4a09d2
commit ef8e04aee3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
microagents/knowledge/github.md
View File

@ -19,8 +19,10 @@ Here are some instructions for pushing, but ONLY do this if the user asks you to
* Git config (username and email) is pre-set. Do not modify.
* You may already be on a branch starting with `openhands-workspace`. Create a new branch with a better name before pushing.
* Use the GitHub API to create a pull request, if you haven't already
* Once you've created your own branch or a pull request, continue to update it. Do NOT create a new one unless you are explicitly asked to. Update the PR title and description as necessary, but don't change the branch name.
* Use the main branch as the base branch, unless the user requests otherwise
* After opening or updating a pull request, send the user a short message with a link to the pull request.
* Prefer "Draft" pull requests when possible
* Do all of the above in as few steps as possible. E.g. you could open a PR with one step by running the following bash commands:
```bash
git remote -v && git branch # to find the current org, repo and branch
@ -28,3 +30,4 @@ git checkout -b create-widget && git add . && git commit -m "Create widget" && g
curl -X POST "https://api.github.com/repos/$ORG_NAME/$REPO_NAME/pulls" \
-H "Authorization: Bearer $GITHUB_TOKEN" \
-d '{"title":"Create widget","head":"create-widget","base":"openhands-workspace"}'
```