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.

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

[Documentation]: Documentation on fixing GitHub issues with OpenDevin #1828

Closed
neubig opened this issue May 16, 2024 · 0 comments · Fixed by #1904
Closed

[Documentation]: Documentation on fixing GitHub issues with OpenDevin #1828

neubig opened this issue May 16, 2024 · 0 comments · Fixed by #1904
Labels
documentation Improvements or additions to documentation enhancement New feature or request severity:medium Problems that affect many users

Comments

@neubig
Copy link
Contributor

neubig commented May 16, 2024

It would be nice to have better documentation on fixing github issues with OpenDevin. This should be added to the documentation in the docs/ directory in the appropriate place.

A first draft of the required documentation is below between the lines:


To fix an issue on OpenDevin, send a prompt like:

Please fix a github issue according to the following procedure:
1. Read the issue on https://github.com/OpenDevin/OpenDevin/issues/1611
2. Clone the repository and check out a new branch
3. Based on the instructions in the issue description, modify files to fix the issue
4. Push the resulting output to github using the GITHUB_TOKEN environment variable
5. Tell me the link that I need to go to to send a pull request

Before you run OpenDevin, you can do

export SANDBOX_ENV_GITHUB_TOKEN=XXX

where XXX is a github token that you created that has permissions to push to the OpenDevin repo. If you don’t have write permission to the OpenDevin repo, you might need to change that to:

4. Push the resulting output to my fork at https://github.com/USERNAME/OpenDevin/ using the GITHUB_TOKEN environment variable

where USERNAME is your github username.


@neubig neubig added documentation Improvements or additions to documentation enhancement New feature or request labels May 16, 2024
@rbren rbren added the severity:medium Problems that affect many users label May 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation enhancement New feature or request severity:medium Problems that affect many users
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants