Stream: coqbot devs & users

Topic: Mangled messages


view this post on Zulip Jason Gross (Jun 09 2021 at 15:10):

What's up with https://github.com/coq/coq/pull/13072#issuecomment-857781670 ?

Additionally, the requested targets ", "performed_via_github_app":null}, "repository":{"id":1377159, "node_id":"MDEwOlJlcG9zaXRvcnkxMzc3MTU5", "name":"coq", "full_name":"coq/coq", "private":false, "owner":{"login":"coq", "id":621198, "node_id":"MDEyOk9yZ2FuaXphdGlvbjYyMTE5OA==", "avatar_url":"https://avatars.githubusercontent.com/u/621198?v=4", "gravatar_id":"", "url":"https://api.github.com/users/coq", "html_url":"https://github.com/coq", "followers_url":"https://api.github.com/users/coq/followers", "following_url":"https://api.github.com/users/coq/following{/other_user}", "gists_url":"https://api.github.com/users/coq/gists{/gist_id}", "starred_url":"https://a
[...]

view this post on Zulip Jason Gross (Jun 09 2021 at 15:22):

Ah, this is a bug I introduced, see https://github.com/coq/bot/commit/be7915e70b973bb401d64a3b754a65a6f74089c3#r51939937, sorry


Last updated: Jan 31 2023 at 09:01 UTC