Skip to content

Conversation

@joshualitt
Copy link
Contributor

"get_pull_request_comments" does not appear to be a valid tool name anymore. I think this is now get_pull_request_review_comments. There are also a few pull request tools which appear to be missing, so those have been added as well.

Copy link
Contributor

@jerop jerop left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can we consolidate this with changes in #354?

#353

@joshualitt
Copy link
Contributor Author

Let's land #354 instead, as it pins to a consistent version.

@joshualitt joshualitt closed this Oct 22, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants