mirror of
https://github.com/OpenHands/OpenHands.git
synced 2025-12-26 05:48:36 +08:00
[Fix]: inconsistent microagent descriptions (#8800)
This commit is contained in:
parent
3f0d8e7f47
commit
10a4ab9199
@ -11,10 +11,11 @@ triggers:
|
||||
You have access to an environment variable, `GITHUB_TOKEN`, which allows you to interact with
|
||||
the GitHub API.
|
||||
|
||||
<IMPORTANT>
|
||||
You can use `curl` with the `GITHUB_TOKEN` to interact with GitHub's API.
|
||||
ALWAYS use the GitHub API for operations instead of a web browser.
|
||||
|
||||
To open a pull request, always use the `create_pr` tool
|
||||
ALWAYS use the `create_pr` tool to open a pull request
|
||||
</IMPORTANT>
|
||||
|
||||
If you encounter authentication issues when pushing to GitHub (such as password prompts or permission errors), the old token may have expired. In such case, update the remote URL to include the current token: `git remote set-url origin https://${GITHUB_TOKEN}@github.com/username/repo.git`
|
||||
|
||||
@ -26,11 +27,9 @@ Here are some instructions for pushing, but ONLY do this if the user asks you to
|
||||
* 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 NOT mark a pull request as ready to review unless the user explicitly says so
|
||||
* 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:
|
||||
* Do all of the above in as few steps as possible. E.g. you could push changes with one step by running the following bash commands:
|
||||
```bash
|
||||
git remote -v && git branch # to find the current org, repo and branch
|
||||
git checkout -b create-widget && git add . && git commit -m "Create widget" && git push -u origin create-widget
|
||||
# Then use the MCP tool to create the PR instead of directly using the GitHub API
|
||||
```
|
||||
|
||||
@ -11,10 +11,11 @@ triggers:
|
||||
You have access to an environment variable, `GITLAB_TOKEN`, which allows you to interact with
|
||||
the GitLab API.
|
||||
|
||||
<IMPORTANT>
|
||||
You can use `curl` with the `GITLAB_TOKEN` to interact with GitLab's API.
|
||||
ALWAYS use the GitLab API for operations instead of a web browser.
|
||||
|
||||
To open a merge request, always use the `create_mr` tool
|
||||
ALWAYS use the `create_mr` tool to open a merge request
|
||||
</IMPORTANT>
|
||||
|
||||
If you encounter authentication issues when pushing to GitLab (such as password prompts or permission errors), the old token may have expired. In such case, update the remote URL to include the current token: `git remote set-url origin https://oauth2:${GITLAB_TOKEN}@gitlab.com/username/repo.git`
|
||||
|
||||
@ -26,10 +27,8 @@ Here are some instructions for pushing, but ONLY do this if the user asks you to
|
||||
* Once you've created your own branch or a merge 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 merge request, send the user a short message with a link to the merge request.
|
||||
* Prefer "Draft" merge 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:
|
||||
* Do all of the above in as few steps as possible. E.g. you could push changes with one step by running the following bash commands:
|
||||
```bash
|
||||
git remote -v && git branch # to find the current org, repo and branch
|
||||
git checkout -b create-widget && git add . && git commit -m "Create widget" && git push -u origin create-widget
|
||||
# Then use the MCP tool to create the MR instead of directly using the GitLab API
|
||||
```
|
||||
|
||||
@ -58,7 +58,7 @@ async def create_pr(
|
||||
title: Annotated[str, Field(description='PR Title')],
|
||||
body: Annotated[str | None, Field(description='PR body')],
|
||||
) -> str:
|
||||
"""Open a draft PR in GitHub"""
|
||||
"""Open a PR in GitHub"""
|
||||
|
||||
logger.info('Calling OpenHands MCP create_pr')
|
||||
|
||||
@ -113,7 +113,7 @@ async def create_mr(
|
||||
title: Annotated[str, Field(description='MR Title')],
|
||||
description: Annotated[str | None, Field(description='MR description')],
|
||||
) -> str:
|
||||
"""Open a draft MR in GitLab"""
|
||||
"""Open a MR in GitLab"""
|
||||
|
||||
logger.info('Calling OpenHands MCP create_mr')
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user