Run pull request jobs

Before merging a pull request on GitHub (or manually via the command line), one needs to be sure that nothing breaks due to the changes made on the pull request.

For that we have some special jenkins job meant for that:

If the pull request targets both 5.2 and 5.1 you need to run a job on each of the jenkins jobs mentioned above.

Test a pull request

To test a pull request with this jenkins job, either:

Run a pull request job

GitHub integration

As soon as the job starts the pull request on GitHub will be notified, showing that the pull request is being tested by

When it finishes, GitHub will be notified again and either report that all tests passed, or that there has been some failures and thus it would not be wise to merge the pull request.

Mail integration

Reporting is not only done via GitHub, but also by email.

When the jenkins job is finished it will report by mail to the user that started the jenkins job.

On the mail, the status of the job and a link to the jenkins job itself and to the pull request(s) are provided for convenience.