Jason Gross (Jun 08 2021 at 23:06): 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?
Théo Zimmermann (Jun 09 2021 at 07:23):Are you sure it's coqbot that truncates them? Could it be GitHub?
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
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: Apr 19 2024 at 12:02 UTC