Skip to content

[Merged by Bors] - chore: bump ProofWidgets to 0.0.15#7070

Closed
kim-em wants to merge 22 commits intomasterfrom
bump_proofwidgets_15
Closed

[Merged by Bors] - chore: bump ProofWidgets to 0.0.15#7070
kim-em wants to merge 22 commits intomasterfrom
bump_proofwidgets_15

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Sep 10, 2023 •
edited by github-actions bot
Loading

We attempted this previously in #7044 and #7056, but it resulted in a broken cache.

Hopefully that is reproducible on this PR, and we can diagnose and fix before merging!

Open in Gitpod

@kim-em kim-em added the WIP Work in progress label Sep 10, 2023
@kim-em kim-em mentioned this pull request Sep 11, 2023
Closed
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 11, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Sep 14, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 14, 2023

This PR/issue depends on:

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 15, 2023
@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Sep 15, 2023 •
edited
Loading

bors merge

@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Sep 15, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Sep 15, 2023

👎 Rejected by label

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 15, 2023
@PatrickMassot PatrickMassot removed the WIP Work in progress label Sep 15, 2023
@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Sep 15, 2023

bors merge

bors bot pushed a commit that referenced this pull request Sep 15, 2023
@kim-em @digama0
chore: bump ProofWidgets to 0.0.15 (#7070)
58a2841 
We attempted this previously in #7044 and #7056, but it resulted in a broken cache.

Hopefully that is reproducible on this PR, and we can diagnose and fix before merging!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 15, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: bump ProofWidgets to 0.0.15 [Merged by Bors] - chore: bump ProofWidgets to 0.0.15 Sep 15, 2023
@bors bors bot closed this Sep 15, 2023
@bors bors bot deleted the bump_proofwidgets_15 branch September 15, 2023 07:15
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@kim-em @digama0 @kodyvajjha
chore: bump ProofWidgets to 0.0.15 (#7070)
6f5d4bd 
We attempted this previously in #7044 and #7056, but it resulted in a broken cache.

Hopefully that is reproducible on this PR, and we can diagnose and fix before merging!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
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

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @PatrickMassot @digama0