2 Commits

Author	SHA1	Message	Date
Xavier Morel	1b5a05e40c	[FIX] mergebot: improve handling of having missed PR updates ... 1. if we try to stage a PR and realize we'd stored / checked the wrong head, cancel the staging and notify the PR 2. provide a command to forcefully update pr heads (or at least check that a PR's head is up to date) Closes #241	2019-11-21 08:10:39 +01:00
Xavier Morel	e52d08ecdf	[ADD] runbot_merge: a merge bot ... No actual dependency on runbot, should be usable completely independently.	2018-09-03 13:16:36 +02:00