Stream: Miscellaneous

Topic: deleting pages doesn't appear in zulip notifications

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 11:27):

https://gitlab.com/coq/wiki/-/commit/cebc0f242151e54cdb858df012c297a7fb4049c4 didn't appear in the notifications stream AFAICT

view this post on Zulip Théo Zimmermann (Jan 26 2022 at 11:47):

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?

view this post on Zulip Cyril Cohen (Jan 26 2022 at 11:57):

I believe this is a missing feature on the github side...

view this post on Zulip Cyril Cohen (Jan 26 2022 at 11:59):

(I do not have access to Coq settings, but in mathcomp) the bot behaviour is controled in Settings > Webhooks > https://coq.zulipchat.com/api/v1/external/github

view this post on Zulip Cyril Cohen (Jan 26 2022 at 11:59):

and then ther is only one box for Wiki

view this post on Zulip Cyril Cohen (Jan 26 2022 at 11:59):

If it does not include deletion, it should be reported to github

view this post on Zulip Théo Zimmermann (Jan 26 2022 at 12:05):

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.

view this post on Zulip Théo Zimmermann (Jan 26 2022 at 13:09):

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: Oct 13 2024 at 01:02 UTC