You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, there are a few github workflows triggered by pull-requests (e.g. ci-linux and ci-macos). As they take too much time to be invoked on every pull request, this triggers should be removed.
The text was updated successfully, but these errors were encountered:
What is the plan to get this ticket now merged? If one allows PRs to the new repo (without merging this ticket first), then the ci will be overloaded quite quickly. Can you open a PR with your commits and merge it before opening up the new repo for the "public"?
Currently, there are a few github workflows triggered by pull-requests (e.g. ci-linux and ci-macos). As they take too much time to be invoked on every pull request, this triggers should be removed.
The text was updated successfully, but these errors were encountered: