diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index bf9f852b9..5d27af671 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -13,7 +13,7 @@ name: push CI on: push: - branches: [ simon ] + branches: [ simon, simon2 ] # Run this workflow for changes to any file, even trivial doc fixes # (since merging to master requires a successful run). # Ideally caching will keep it relatively cheap; avoid over-pushing.