How do I extract the base and head sha of a PR from a not-necessarily-review comment on the issue? I'm told https://github.com/Zimmi48/bot/blob/faddaa3ea924e3e44ab575e8de0b261ae3970ce9/src/actions.ml#L1208-L1229 is wrong
You should send a specific request, such as
Thanks! I've updated the code and am re-deploying it now
According to the bot log, that seems to give me a quoted version of the sha. Is this supposed to happen? https://github.com/JasonGross/bot/blob/f05e35f667b66c10930cf1e9a7d1de0c1d5f2f09/src/actions.ml#L616
19 May 2021 07:02:39.565161 <190>1 2021-05-19T11:02:39.005686+00:00 app web.1 - - I'm going to look for failed tests to minimize on PR #14037 failed. 19 May 2021 07:02:39.917157 <190>1 2021-05-19T11:02:39.316605+00:00 app web.1 - - Error while attempting to find jobs to minimize from PR #14037: 19 May 2021 07:02:39.917222 <190>1 2021-05-19T11:02:39.316619+00:00 app web.1 - - Error while looking for failed library tests to minimize: Unkown base commit coq/coq@"737b74d92dd07c7396a40205c0d9b72d45d3a137".
Oh, right! This is a known issue. See https://github.com/coq/bot/issues/61
Last updated: May 28 2023 at 18:29 UTC