Do not run the CI workflow on pull requests.

There's a separate PR workflow that does fewer tasks.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 43278b98c2acec42444f16e1da402d58f1c20f6a..4ceea8ac995df8c3862f0ea59fbb25c6f0f6ab6d 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -3,8 +3,6 @@ name: CI
 on:
   push:
     branches: [ master ]
-  pull_request:
-    branches: [ master ]
 
 jobs:
   build: