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

Reopening of previous PR #309

Merged
merged 262 commits into from
Dec 12, 2021
Merged

Reopening of previous PR #309

merged 262 commits into from
Dec 12, 2021

Conversation

torfjelde
Copy link
Member

@torfjelde torfjelde commented Aug 19, 2021

What we need before merge:

  1. Updated benchmarks.
  2. Resolve comments.

torfjelde and others added 30 commits June 1, 2021 00:43
Co-authored-by: David Widmann <devmotion@users.noreply.github.com>
Co-authored-by: David Widmann <devmotion@users.noreply.github.com>
Co-authored-by: David Widmann <devmotion@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Dec 8, 2021
What we need before merge:
1. [x] Updated benchmarks.
2. [ ] Resolve comments.

Co-authored-by: Hong Ge <hg344@cam.ac.uk>
@bors
Copy link
Contributor

bors bot commented Dec 8, 2021

Build failed:

@torfjelde
Copy link
Member Author

bors try

@bors
Copy link
Contributor

bors bot commented Dec 11, 2021

try

Already running a review

@torfjelde
Copy link
Member Author

bors try

@bors
Copy link
Contributor

bors bot commented Dec 11, 2021

try

Already running a review

@torfjelde
Copy link
Member Author

bors try

@bors
Copy link
Contributor

bors bot commented Dec 11, 2021

try

Already running a review

@yebai
Copy link
Member

yebai commented Dec 11, 2021

Bors try

@bors
Copy link
Contributor

bors bot commented Dec 11, 2021

try

Already running a review

@yebai
Copy link
Member

yebai commented Dec 11, 2021

Let me know if you want me to merge this PR manually - Bors seems on strike again. @torfjelde

@yebai yebai merged commit 1744ba7 into master Dec 12, 2021
@yebai yebai deleted the tor/simple-varinfo-v2 branch December 12, 2021 10:27
@bors
Copy link
Contributor

bors bot commented Dec 12, 2021

try

Timed out.

bors bot pushed a commit that referenced this pull request Dec 14, 2021
#309 was merged a bit too soon, for example `bors` was never run on the final version due to some issues. Before we make a release, we should make sure that it all works properly.
bors bot pushed a commit that referenced this pull request Dec 14, 2021
#309 was merged a bit too soon, for example `bors` was never run on the final version due to some issues. Before we make a release, we should make sure that it all works properly.
bors bot pushed a commit that referenced this pull request Dec 14, 2021
#309 was merged a bit too soon, for example `bors` was never run on the final version due to some issues. Before we make a release, we should make sure that it all works properly.
bors bot pushed a commit that referenced this pull request Dec 14, 2021
#309 was merged a bit too soon, for example `bors` was never run on the final version due to some issues. Before we make a release, we should make sure that it all works properly.
bors bot pushed a commit that referenced this pull request Dec 14, 2021
#309 was merged a bit too soon, for example `bors` was never run on the final version due to some issues. Before we make a release, we should make sure that it all works properly.
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.

None yet

4 participants