PRs

[Rainer Müller]

On 19.05.19 20:45, Christopher Chavez wrote:
> On 5/19/2019 1:40 PM, Mark Anderson wrote:
>> making it possible to re-run CI from GitHub commits.
> 
> As a PR submitter, one workaround I'm aware of is rebasing the PR
> commit(s). I'm not sure that's something members can/should try though,
> so a better solution is probably still preferred…

I would not consider this a workaround, but the best choice we have.

Re-running the build with the exact same revision would not be that
useful. Without changes to the source, I would expect the same result.
As the ports tree and therefore the dependencies have usually advanced
since the PR was submitted, it makes sense to do a rebase first before
attempting another build.

In theory it is possible to restart a build on the Travis CI web
interface with the same revision, but I am not even sure if all members
have access to that?

Rainer