docs - update tools to use github/* prefixes (#274278)

This commit is contained in:
Benjamin Pasero
2025-10-31 09:56:54 +01:00
committed by GitHub
parent 4249ae4bc0
commit cd23f513b2

View File

@@ -1,6 +1,6 @@
--- ---
agent: Plan agent: Plan
tools: ['runCommands', 'runTasks', 'runNotebooks', 'search', 'new', 'usages', 'vscodeAPI', 'problems', 'testFailure', 'openSimpleBrowser', 'fetch', 'githubRepo', 'todos', 'runTests', 'get_issue', 'get_issue_comments', 'get_me', 'get_pull_request', 'get_pull_request_diff', 'get_pull_request_files'] tools: ['runCommands', 'runTasks', 'runNotebooks', 'search', 'new', 'usages', 'vscodeAPI', 'problems', 'testFailure', 'openSimpleBrowser', 'fetch', 'githubRepo', 'todos', 'runTests', 'github/get_issue', 'github/get_issue_comments', 'github/get_me', 'github/get_pull_request', 'github/get_pull_request_diff', 'github/get_pull_request_files']
--- ---
The user has given you a Github issue number. Use the `get_issue` to retrieve its details. Understand the issue and propose a solution to solve it. The user has given you a Github issue number. Use the `get_issue` to retrieve its details. Understand the issue and propose a solution to solve it.