mikepapadim commented on issue #8673: URL: https://github.com/apache/tvm/issues/8673#issuecomment-895324328
> Thanks for bringing this up! I was thinking about this issue while ago but didn't take actions... > Another though is moving the docs building process from Jenkins to Github actions. In this case, we don't even need to use the CI resources when only changing docs. I think if it possible to move the CI to GH actions only for doc changes, it will remove a lot of overhead from the current Jenkins workers. -- 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]
