Zulip Chat Archive
Stream: general
Topic: doc-gen fails
Gabriel Ebner (Jul 30 2020 at 20:51):
Speaking of github action notification spam, apparently 1) I get it for cron jobs on the doc-gen repo, and 2) doc generation is broken today:
https://github.com/leanprover-community/doc-gen/runs/929308222
Rob Lewis (Jul 30 2020 at 21:06):
Huh. My guess in the other thread was wrong then, I set that up, didn't I?
Rob Lewis (Jul 30 2020 at 21:06):
Oh, but you merged it.
Rob Lewis (Jul 30 2020 at 21:07):
No clue what the breakage is. I'll look into it tomorrow.
Gabriel Ebner (Jul 31 2020 at 07:36):
I'm now getting an email every two hours.
Rob Lewis (Jul 31 2020 at 08:17):
I'm on it now.
Rob Lewis (Jul 31 2020 at 08:36):
Docs are back, spam bot is gone!
Last updated: Dec 20 2023 at 11:08 UTC