Stream: coqbot devs & users

Topic: truncated comments?


view this post on Zulip Jason Gross (Jun 08 2021 at 23:06):

coqbot seems to be truncating comments before posting them, as in https://github.com/coq/coq/pull/13126#issuecomment-856089252. Any ideas what's going on?

view this post on Zulip Théo Zimmermann (Jun 09 2021 at 07:23):

Are you sure it's coqbot that truncates them? Could it be GitHub?

view this post on Zulip Jason Gross (Jun 09 2021 at 13:44):

As @Gaëtan Gilbert tested by editing that comment, GitHub still seems to allow longer comments. And when I've tried posting comments above GitHub's limits in the past, GitHub just gives me an error and refuses to post any comments, so I've carefully truncated the subparts of the comments so that the whole comment fits within GitHub's limits

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

Oh, I just found a bug in the truncation code, so it's possible that I messed up the calculations enough for this to happen


Last updated: Jan 31 2023 at 09:01 UTC