tree 1213dbc66bf61d0a8d60dd0fe250a58cd06eb847
parent 00180e1fcb1ceaadacc14f5585a043fa53f80882
author Luca Milanesio <luca.milanesio@gmail.com> 1381393631 +0100
committer Luca Milanesio <luca.milanesio@gmail.com> 1381500732 +0000

Make GitHub job pool configurable via gerrit.config.

Allows limiting the number of parallel jobs and their
scheduled execution time via gerrit.config properties.

Example:
[github]
        jobPoolLimit = 1
        jobExecTimeout = 10

The above configuration will limit to 1 concurrent
GitHub API executed with a random interval of 10 secs
between calls.

Randomisation and limitation of GitHub API execution
is needed in order to avoid going over the maximum
threshold allowed by GitHub front-end servers.
(they are very aggressive nowadays, after the outages
and DDoS they've experienced)

Change-Id: Ib273dbb9f42640b841d98d58565771f6a0157518