You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
}
?
I doubt that this will work
The text was updated successfully, but these errors were encountered:
msprotz
changed the title
VSTS: post-commit hook?
Make the bot go through the normal branch-green-merge process
Dec 8, 2016
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_branch
where
?
I doubt that this will work
The text was updated successfully, but these errors were encountered: