From b1ee298640b066c2606b7bd3bfd257b160cdcf35 Mon Sep 17 00:00:00 2001
From: Robert Hensing <robert@roberthensing.nl>
Date: Sun, 18 Dec 2022 00:02:06 +0100
Subject: [PATCH] Poke github

The last PR was merged at the git layer, but the GitHub UI doesn't
show the merged state.
Furthermore, webhooks from this action have not arrived at
Hercules CI, or the GitHub Apps dashboard for webhooks for that
matter.

Maybe another push event will kick things back into action?