Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Cleanup error messages that should not contain the string TODO #617

Merged
merged 1 commit into from
Jul 11, 2023

Conversation

jonasbb
Copy link
Owner

@jonasbb jonasbb commented Jul 11, 2023

bors r+

@bors
Copy link
Contributor

bors bot commented Jul 11, 2023

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot merged commit e096f0b into master Jul 11, 2023
@bors bors bot deleted the update-error-message branch July 11, 2023 22:39
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant