Skip to content

feat: add tool for checking if PR is merged #241

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

Closed

Conversation

simondanielsson
Copy link
Contributor

@simondanielsson simondanielsson commented Apr 12, 2025

This PR adds a tool for checking if a pull request is merged.

Closes: #240

Implementation detail: two possible responses from the API endpoint:

  • 204: has been merged
  • 404: either has not been merged, or PR does not exists. Note: I could not find a way to discern between these two cases - happy to hear your thoughts/suggestions on how to potentially fix this.

Example output

$ ./mcpcurl --stdio-server-cmd "./github-mcp-server stdio" tools is_pull_request_merged --owner github --repo github-mcp-server --pullNumber 235
{
  "status": "Pull request not merged or does not exist."
}

$ ./mcpcurl --stdio-server-cmd "./github-mcp-server stdio" tools is_pull_request_merged --owner github --repo github-mcp-server --pullNumber 239
{
  "status": "Pull request is merged."
}

Testing done:

go mod tidy
go mod vendor
go mod verify
go fmt ./...
go vet ./...
golangci-lint run
go test -v ./...

and mcpcurl commands in example above.

@juruen
Copy link
Collaborator

juruen commented Apr 13, 2025

@simondanielsson I believe this is already covered by get_pull_request:

Screenshot 2025-04-13 at 10 44 40

Your change has the advantage of using less context because the answer is more succinct. However, we are also planning to trim down the responses of the current ones to make a better use of the context.

So as it is now, I'm leaning towards trying to use the existing get_pull_request to avoid adding an extra tool. Let me know what you think!

In any case, thank you for this and your other PRs!

@simondanielsson
Copy link
Contributor Author

I completely missed that - I agree, let's not add another tool specifically for this. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add tool for checking if a pull request is merged
3 participants