Hi, I'm trying out bors for the first time. I tried to merge a PR that purposely fails CI with "bors merge". Then, I closed the PR. I noticed that bors didn't seem to remove the PRs from the queue, and still had them in the "waiting to run" section on the dash. Is that the desired behavior? Is there a way to configure bors to remove PRs from the queue when they are closed?
Thanks for any help anyone can provide! Screenshot of the dash is below- both of those PRs were actually closed on GitHub.