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.

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

build: enforce formatting #741

Closed
wants to merge 2 commits into from
Closed

build: enforce formatting #741

wants to merge 2 commits into from

Conversation

mightyiam
Copy link
Contributor

No description provided.

@mightyiam mightyiam marked this pull request as ready for review August 27, 2023 16:05
@mightyiam
Copy link
Contributor Author

Could anyone please approve workflow, just for the purpose of seeing it fail?

@mightyiam
Copy link
Contributor Author

Rebased. Please approve workflow and review.

@mightyiam
Copy link
Contributor Author

Oh, and we did confirm enforcement works (the first commit) in this run.

@mightyiam
Copy link
Contributor Author

Unsurprisingly, the checks passed. There is no good time to merge this. It may upset contributors with open pull requests. There are 40 open pull requests. Yet, that number might not decrease. Therefore, it may never be less painful than now to merge this. And it's only a click away! :shipit: 😉

@Philippe-Cholet
Copy link
Member

@mightyiam There was a recent important discussion about enforcing formatting anyway in #702 (that and more...). I guess it's currently delayed the time to try to implement some RFC.

@mightyiam
Copy link
Contributor Author

Thanks. Let us know here, as soon as we can pull the trigger on this. The first commit is the enforcement part. The second is merely the result of $ cargo fmt.

@Philippe-Cholet
Copy link
Member

#744 bumped actions/checkout to v4, I guess you might want to do the same.

@mightyiam
Copy link
Contributor Author

Thank you. Done.

@jswrenn jswrenn mentioned this pull request Sep 15, 2023
Merged
@jswrenn
Copy link
Member

jswrenn commented Sep 15, 2023

Thank you! I'm closing this in favor of #751 (which is just a replay of the commits), for reasons explained there.

@jswrenn jswrenn closed this Sep 15, 2023
@mightyiam mightyiam deleted the fmt branch September 15, 2023 15:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mightyiam @Philippe-Cholet @jswrenn