https://gitlab.com/coq/wiki/-/commit/cebc0f242151e54cdb858df012c297a7fb4049c4 didn't appear in the notifications stream AFAICT
That's annoying, because this is the main feed I use (and I guess most of us use) to monitor changes to the wiki. @Cyril Cohen Any idea where to report this issue with the GitHub integration?
I believe this is a missing feature on the github side...
(I do not have access to Coq settings, but in mathcomp) the bot behaviour is controled in
and then ther is only one box for
If it does not include deletion, it should be reported to github
Indeed, it only mentions "Wiki page updated". I looked into the webhook delivery logs, and there doesn't seem to be any log for this event.
I've sent feedback to GitHub, but I don't expect this to be fixed soon, so we might want to consider another monitoring method (e.g., notifications for pushes to the GitLab wiki mirror).
Last updated: Jun 05 2023 at 09:01 UTC