leandron edited a comment on issue #9591: URL: https://github.com/apache/tvm/issues/9591#issuecomment-979427195
> noticed this as well. Note that unfortunately we all do not have perm to push to main(all committers have the same access perm). We will need to figure out a way, perhaps change jenkins policy temporarily to trust Jenkinsfile from PR from certain users Oh I didn't know we don't have access to manually push to main. So I guess you have set the Jenkins configuration in the job to trust certain users and the current job on #9592 is running with the actual proposed Jenkinsfile? So, given that, we just need for CI to complete and then merge that fix? -- 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]
