Why didn't this PR get labeled?

[Rainer Müller]

On 2018-05-01 16:28, Perry E. Metzger wrote:
> On Tue, 1 May 2018 13:20:45 +0000 Zero King <l2dy at macports.org> wrote:
>> As Rainer replied, GitHub didn't provide the needed information in
>> time. Maybe we should wait 30 seconds and retry?
> 
> That seems like a very good idea. I'd probably wait two minutes,
> though, just to nail it.

This should be reported to GitHub support. I would consider it a bug at
their end if they send out WebHooks but do not actually provide the
referenced data via the API yet.

Rainer