Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(linear_algebra/matrix/sesquilinear_form): fix a timeout #17705

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(linear_algebra/matrix/sesquilinear_form): fix a timeout #17705

wants to merge 1 commit into from

Conversation

riccardobrasca
Copy link
Member

Open in Gitpod

@riccardobrasca riccardobrasca added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. labels Nov 24, 2022
@mcdoll
Copy link
Member

mcdoll commented Nov 24, 2022

maintainer merge

@github-actions
Copy link

🚀 Pull request has been placed on the maintainer queue by mcdoll.

jcommelin
jcommelin approved these changes Nov 24, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 24, 2022
@eric-wieser eric-wieser mentioned this pull request Nov 24, 2022
Closed
bors bot pushed a commit that referenced this pull request Nov 24, 2022
@riccardobrasca
chore(linear_algebra/matrix/sesquilinear_form): fix a timeout (#17705)
bb0ad86
@bors
Copy link

bors bot commented Nov 24, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(linear_algebra/matrix/sesquilinear_form): fix a timeout [Merged by Bors] - chore(linear_algebra/matrix/sesquilinear_form): fix a timeout Nov 24, 2022
@bors bors bot closed this Nov 24, 2022
@bors bors bot deleted the RB/timeout branch November 24, 2022 13:50
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@riccardobrasca @mcdoll @jcommelin @leanprover-community-bot-assistant