Skip to content
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

Update to remove const_err #114

Closed
wants to merge 1 commit into from

Conversation

marcsvll
Copy link
Contributor

This PR only removed const_err since it will be a hard error in future: rust-lang/rust#71800

Signed-off-by: Marcus de Lima marcus.lima@azion.com

Signed-off-by: Marcus de Lima <marcus.lima@azion.com>
@wiktor-k
Copy link
Collaborator

wiktor-k commented Jan 4, 2023

🤔 Hmm... it seems the CI broke since a couple of new lints were enabled (unnecessary cast). Would you mind also fixing them? (They look relatively minor)

@marcsvll
Copy link
Contributor Author

marcsvll commented Jan 4, 2023

🤔 Hmm... it seems the CI broke since a couple of new lints were enabled (unnecessary cast). Would you mind also fixing them? (They look relatively minor)

I'll check it out.

@wiktor-k
Copy link
Collaborator

It seems #117 fixed the CI issues so if you rebased your changes on top of main and force push it should work.

Copy link
Member

@ionut-arm ionut-arm left a comment

Choose a reason for hiding this comment

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

A bit late on my side, but thanks! I think we can simply rebase and merge, the change should apply equally well despite the other stuff that's been merged. @wiktor-k - what do you think?

@wiktor-k
Copy link
Collaborator

A bit late on my side, but thanks! I think we can simply rebase and merge, the change should apply equally well despite the other stuff that's been merged. @wiktor-k - what do you think?

Yep, agreed. I actually contacted the author via email but have not heard back. Then I thought the same, it's a simple fix, let's just rebase and merge but then other stuff came up. Let's merge this asap and get on with other PRs.

@wiktor-k
Copy link
Collaborator

wiktor-k commented Jan 24, 2023

I'm going to replace this PR with #122 while preserving authorship. Thanks for your contribution @marcsvll!

@wiktor-k wiktor-k closed this Jan 24, 2023
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.

3 participants