@@ -101,37 +101,3 @@ Sometimes, we tend to only interact with people we know.
101101However, broad collaborations are necessary to the success of the project.
102102Try to keep that in mind, shepherd PRs for, and request code reviews from
103103community members who you do not interact physically.
104-
105-
106- Keeping CI Green
107- ----------------
108- Developers rely on the TVM CI to get signal on their PRs before merging.
109- Occasionally breakges slip through and break ``main ``, which in turn causes
110- the same error to show up on an PR that is based on the broken commit(s).
111- In these situations it is possible to either revert the offending commit or
112- submit a forward fix to address the issue. It is up to the committer and commit
113- author which option to choose, keeping in mind that a broken CI affects all TVM
114- developers and should be fixed as soon as possible.
115-
116- For reverts and trivial forward fixes, adding ``[skip ci] `` to the revert's
117- commit message will cause CI to shortcut and only run lint. Committers should
118- take care that they only merge CI-skipped PRs to fix a failure on ``main `` and
119- not in cases where the submitter wants to shortcut CI to merge a change faster.
120-
121- .. code :: bash
122-
123- # Example: Skip CI on a revert
124- # Revert HEAD commit, make sure to insert '[skip ci]' at the beginning of
125- # the commit subject
126- git revert HEAD
127-
128- git checkout -b my_fix
129- # After you have pushed your branch, create a PR as usual.
130- git push my_repo
131-
132- # Example: Skip CI on a branch with an existing PR
133- # Adding this commit to an existing branch will cause a new CI run where
134- # Jenkins is skipped
135- git commit --allow-empty --message " [skip ci] Trigger skipped CI"
136- git push my_repo
137-
0 commit comments