Jason Gross (May 17 2021 at 20:27): Jason Gross (May 17 2021 at 20:27):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
Théo Zimmermann (May 18 2021 at 06:54):You should send a specific request, such as get_pull_request_refs (https://github.com/coq/bot/blob/b10cfb9dd8aea4eb5865f3d636123f1794312eca/bot-components/GitHub_queries.mli#L30-L35).
Jason Gross (May 18 2021 at 15:05):Thanks! I've updated the code and am re-deploying it now
Jason Gross (May 19 2021 at 11:32):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