You are viewing a plain text version of this content. The canonical link for it is here.

Posted to commits@tvm.apache.org by GitBox <gi...@apache.org> on 2022/12/09 00:19:16 UTC

[GitHub] [tvm] driazati commented on pull request #13475: [ci] Don't merge PRs with main

driazati commented on PR #13475:
URL: https://github.com/apache/tvm/pull/13475#issuecomment-1343615337

   Some more context / notes around this from offline discussion with @areusch and @tqchen:
   
   * Right now merging with main prevents some issues around merge-racing PRs (e.g. a big refactor merges but a PR is put up based on an older commit and uses the old APIs), if these happen with any frequency we should just revert this change
   * We should integrate into our reporting better an explanation of what CI is doing with the code it runs (i.e. print out the commit to merge with before running unit tests to reproduce what CI actually did) if we end up not keeping this PR
   


-- 
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: commits-unsubscribe@tvm.apache.org

For queries about this service, please contact Infrastructure at:
users@infra.apache.org