areusch opened a new issue, #11473: URL: https://github.com/apache/tvm/issues/11473
it would be helpful if we also allow folks to retrigger the CI. we can't recognize force-pushes because GH garbage-collects the old pushes, but if ppl push an empty or merge commit we could check whether or not anything was changed and allow it to merge. this would let folks fix trivial CI problems without requiring re-approval. cc @driazati -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
