Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
ci: don't run heavy ci on push to main (#295)
Due to extensive use of the merge queue, we essentially run the heavy ci twice. once in the merge group and then again when being pushed from the merge group to main. This wastes runner resources and time. Instead we can just run on schedule every night and count on the merge group CI runs. Signed-off-by: simonsan <[email protected]>
- Loading branch information