sync-mailing-list-mirror: force push on workflow_dispatch

Signed-off-by: Johannes Schindelin <[email protected]>

Author: dscho

.github/workflows/sync-mailing-list-mirror.yml

@@ -26,6 +26,10 @@ jobs:
         set -x
         echo "org=${TARGET_GITHUB_REPOSITORY%%/*}" >>$GITHUB_OUTPUT &&
         echo "repo=${TARGET_GITHUB_REPOSITORY#*/}" >>$GITHUB_OUTPUT &&
+        test workflow_dispatch != '${{ github.event_name }}' || {
+          echo "result=true" >>$GITHUB_OUTPUT
+          exit 0
+        }
         source="$(git ls-remote "$SOURCE_REPOSITORY" master)" &&
         target="$(git ls-remote https://github.com/"$TARGET_GITHUB_REPOSITORY" lore-$LORE_EPOCH)" &&
         echo "result=$(test "${source%%	*}" = "${target%%	*}" && echo false || echo true)" >>$GITHUB_OUTPUT