Started 1 mo 23 days ago
Took 31 min

Build #5768 (Jul 26, 2021, 9:35:14 PM)

PR #4187: Delete disused parallel_red...

GitHub pull request #4187 of commit ef61246183268ebe06a304a589519064315dd75d, no merge conflicts.