Regression workers attempt to fetch up-to-date references from the CakeML remote to update their local repos:
head commits for normal branches
head commits for pull requests
Normal branches are named as in the remote, but pull requests are renamed to pr/<pr_number> locally. This causes a name clash when there is a normal branch which already has the name pr/<pr_number>, producing errors like the following:
fatal: Cannot fetch both refs/heads/pr/991 and refs/pull/991/head to refs/heads/pr/991
/usr/bin/git failed on fetch --prune origin +refs/heads/*:refs/heads/* +refs/pull/*/head:refs/heads/pr/*
This PR attempts to improve the situation by avoiding the renaming. So the pull request branches are now named refs/pull/<pr_number>/head.
Two things to note:
This may not completely avoid name clashes - it might be possible to cause one by naming a branch refs/pull/<pr_number>/head.
Disclaimer: I don't know why the branches were renamed in the first place, so if there was a particular reason then this PR may break something.
Regression workers attempt to fetch up-to-date references from the CakeML remote to update their local repos:
Normal branches are named as in the remote, but pull requests are renamed to
pr/<pr_number>locally. This causes a name clash when there is a normal branch which already has the namepr/<pr_number>, producing errors like the following:This PR attempts to improve the situation by avoiding the renaming. So the pull request branches are now named
refs/pull/<pr_number>/head.Two things to note:
refs/pull/<pr_number>/head.