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

Jump to bottom

CI: Add clippy workflow #48

Merged
merged 4 commits into from
Dec 29, 2021
Merged

CI: Add clippy workflow #48

merged 4 commits into from
Dec 29, 2021

Conversation

mkroening
Copy link
Member

No description provided.

@mkroening mkroening requested a review from stlankes December 12, 2021 23:08
@mkroening mkroening force-pushed the clippy branch 2 times, most recently from 02c64e1 to 5051eb7 Compare December 13, 2021 17:13
@mkroening
Copy link
Member Author

bors r+

bors bot added a commit that referenced this pull request Dec 21, 2021
@bors @mkroening
Merge #48
4480b9f 
48: CI: Add clippy workflow r=mkroening a=mkroening



Co-authored-by: Martin Kröning <mkroening@posteo.net>
@bors
Copy link
Contributor

bors bot commented Dec 21, 2021

Build failed:

stlankes
stlankes approved these changes Dec 29, 2021
View reviewed changes
Copy link
Contributor

@stlankes stlankes left a comment

Choose a reason for hiding this comment

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

It is Ok, if we merge #50 to the master branch.

@stlankes
Copy link
Contributor

bors r+

@bors
Copy link
Contributor

bors bot commented Dec 29, 2021

Merge conflict.

@stlankes
Copy link
Contributor

bors r+

bors bot added a commit that referenced this pull request Dec 29, 2021
@bors @mkroening @stlankes
Merge #48
ca19a14 
48: CI: Add clippy workflow r=stlankes a=mkroening



Co-authored-by: Martin Kröning <mkroening@posteo.net>
Co-authored-by: Stefan Lankes <stlankes@users.noreply.github.com>
@bors
Copy link
Contributor

bors bot commented Dec 29, 2021

Build failed:

@stlankes
Copy link
Contributor

bors r+

@bors
Copy link
Contributor

bors bot commented Dec 29, 2021

Build succeeded:

@bors bors bot merged commit 769c9af into master Dec 29, 2021
@bors bors bot deleted the clippy branch December 29, 2021 17:24
@mkroening mkroening restored the clippy branch December 29, 2021 17:53
@mkroening mkroening deleted the clippy branch December 29, 2021 17:53
# for free to join this conversation on GitHub. Already have an account? # to comment
Reviewers

@stlankes stlankes stlankes approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@mkroening @stlankes