There is currently a bug where we fail to create a local GitHub PR comment because we haven't imported `time` (or cat the result of `time.time()` to an integer).
<rdar://problem/117472023>
Pull request: https://github.com/WebKit/WebKit/pull/19535
Committed 269767@main (e7164442f39a): <https://commits.webkit.org/269767@main> Reviewed commits have been landed. Closing PR #19535 and removing active labels.