Skip to content

[ci] Separate the ci scripts into Github and Jenkins scripts#12940

Closed
gigiblender wants to merge 1 commit intoapache:mainfrom
gigiblender:separate-scripts
Closed

[ci] Separate the ci scripts into Github and Jenkins scripts#12940
gigiblender wants to merge 1 commit intoapache:mainfrom
gigiblender:separate-scripts

Conversation

@gigiblender
Copy link
Copy Markdown
Contributor

This PR separates the files in the ci/scripts directory into ci/scripts/jenkins and ci/scripts/github. This is done because the github scripts should not be protected in the CI. #12604

@gigiblender gigiblender closed this Oct 5, 2022
driazati pushed a commit that referenced this pull request Nov 14, 2022
This PR is a duplicate of #12940 and #12941. For some reason, I am unable to reopen #12940.
xinetzone pushed a commit to daobook/tvm that referenced this pull request Nov 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant