BORS was working perfectly in github.com/hgrecco/pint until it stopped working for reasons I have not been able to understand. I have tried uninstalling and reinstalling bors without any success. And also now the PRs do not appear int he DashBoard. Any suggestions how to proceed?
An Travis says:
The command "eval git clone --depth=50 --branch=staging.tmp https://github.com/hgrecco/pint.git hgrecco/pint " failed. Retrying, 1 of 3.
Found the cause of your woes (and it has nothing to do with the staging.tmp error):
Notice how https://github.com/hgrecco/pint/pull/605 refers to an "unknown repository" in GitHub's UI? Bors kinda choked on it. You should probably close it, since it won't be possible to merge it successfully and I'm going to make a patch so that bors can sensibly ignore the malformed PR.
Thanks for the response. It seems to work now. Shouldn’t bors automatically skip this?