Skip to content

fix progress report being deduplicated #2524

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

Merged
merged 3 commits into from
Aug 31, 2022
Merged

Conversation

RalfJung
Copy link
Member

Fixes #2522

@RalfJung
Copy link
Member Author

@bors r+

@bors
Copy link
Contributor

bors commented Aug 31, 2022

📌 Commit d91587c has been approved by RalfJung

It is now in the queue for this repository.

@bors
Copy link
Contributor

bors commented Aug 31, 2022

⌛ Testing commit d91587c with merge 5b33f34...

bors added a commit that referenced this pull request Aug 31, 2022
fix progress report being deduplicated

Fixes #2522
@bors
Copy link
Contributor

bors commented Aug 31, 2022

💔 Test failed - checks-actions

@RalfJung
Copy link
Member Author

@bors retry

@RalfJung
Copy link
Member Author

@bors r+

@bors
Copy link
Contributor

bors commented Aug 31, 2022

📌 Commit b08ccb5 has been approved by RalfJung

It is now in the queue for this repository.

@bors
Copy link
Contributor

bors commented Aug 31, 2022

⌛ Testing commit b08ccb5 with merge db2b866...

bors added a commit that referenced this pull request Aug 31, 2022
fix progress report being deduplicated

Fixes #2522
@bors
Copy link
Contributor

bors commented Aug 31, 2022

💔 Test failed - checks-actions

@RalfJung
Copy link
Member Author

@bors r+

@bors
Copy link
Contributor

bors commented Aug 31, 2022

📌 Commit ee585c4 has been approved by RalfJung

It is now in the queue for this repository.

bors added a commit that referenced this pull request Aug 31, 2022
fix progress report being deduplicated

Fixes #2522
@bors
Copy link
Contributor

bors commented Aug 31, 2022

⌛ Testing commit ee585c4 with merge 3b4984f...

@bors
Copy link
Contributor

bors commented Aug 31, 2022

💔 Test failed - checks-actions

@RalfJung
Copy link
Member Author

@bors r+

@bors
Copy link
Contributor

bors commented Aug 31, 2022

📌 Commit 1135ad3 has been approved by RalfJung

It is now in the queue for this repository.

@bors
Copy link
Contributor

bors commented Aug 31, 2022

⌛ Testing commit 1135ad3 with merge 95b315d...

@bors
Copy link
Contributor

bors commented Aug 31, 2022

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 95b315d to master...

@bors bors merged commit 95b315d into rust-lang:master Aug 31, 2022
@RalfJung RalfJung deleted the progress-report branch September 1, 2022 08:50
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.

-Zmiri-report-progress does not keep reporting for infinite loops
2 participants