tree 890785f42a7a4ab295a9c9cea7c2abf969a2d8d2
parent ad2a37ad725369c84d207eed3ff68a91e3932974
author Luca Milanesio <luca.milanesio@gmail.com> 1403108043 +0100
committer David Pursehouse <david.pursehouse@sonymobile.com> 1403251934 +0000

Exclude Gerrit-only repos from GH pull requests

Automatically skip repositories that exist only
in the Gerrit domain when need to fetch GitHub
pull requests.

Before this change the existence of a single repo
in Gerrit that did not exist on GitHub was causing
the GitHub pull request action to fail, without even
a feedback to the end user :-(

Change-Id: Ie4d4dde3a7480f2c0d92eb0d4bc12915a4542482