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.

Sign up for GitHub

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

Jump to bottom

GitHub Actions bot: Prune search space with '--search' #9445

Merged

Mytherin merged 1 commit into duckdb:main from szarnyasg:actions-bot-prune-search-space

Oct 24, 2023

Collaborator

szarnyasg commented Oct 23, 2023 •

edited

Loading

The current bot does not find the matching internal issues when it is an old one due to pagination. This fix resolves this problem.


          GitHub Actions bot: Prune search space with '--search'

a4172e3

szarnyasg requested a review from Mytherin

October 23, 2023 15:12

Mytherin merged commit 4c28a71 into duckdb:main

Collaborator

Mytherin commented Oct 24, 2023

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet