Right now the hint auto-regeneration thing (target: fstar-nightly) relies on dzomo, the bot, being administrator on the F* project because of the branch restriction.
This is unfortunate and weakens security.
If we give the bot just write access, then the bot will have to push to a branch, get a green, and merge into master.
This can be achieved by putting MERGEME in the commit message, then pushing to branch dzomo. Then, the next job (target: fstar-ci), upon getting a green on the branch, will try to merge it.
However, how can we delay the merge & push of the branch to master, long enough so that VSTS gives that goddamn green to GitHub?
nohup merge_branch
where
merge_branch () {
sleep 60 # long enough for GitHub to receive a green
}
Right now the hint auto-regeneration thing (target: fstar-nightly) relies on dzomo, the bot, being administrator on the F* project because of the branch restriction.
nohup merge_branchwhere
?
I doubt that this will work