Might there be a third option of creating a different jenkins job for PR
change and manual triggers? It would clutter up the jenkins interface a
bit, but they could both post status to the same commitStatusContext on
Github, so no one would notice there.
On Wed, Jun 13, 2018 at 11:14 PM Jason Kuster <[EMAIL PROTECTED]>