From cd945297b26def695fb8a7f45eab4fbbaaa61650 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20M=C3=BCller?= Date: Tue, 18 Jul 2023 09:59:29 -0700 Subject: [PATCH] CI: Run CI workflow on pull requests MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Let's run the CI workflow on pull requests, so that feedback is more immediate (well, to the degree that is possible). The only concern here could be that we now potentially run twice when creating a pull request and then merging it. But that seems like a tiny price to pay. If we were to force pull request creation we could remove running on push, but I am not sure that's worth it. Signed-off-by: Daniel Müller --- .github/workflows/ci.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d1e18e9..942047c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,7 @@ name: CI -on: push +on: + pull_request: + push: jobs: test-gnu: