github-ci: don't run builds on PR if only docs changed

diff --git a/.github/workflows/builds.yml b/.github/workflows/builds.yml
index 1b53c35523d4f1d3ed6c61582fb8e4cbdddba7d1..f0e359464f9381c9c69d23646c896795f9bd583d 100644 (file)
--- a/.github/workflows/builds.yml
+++ b/.github/workflows/builds.yml
@@ -7,6 +7,10 @@ on:
       # modified.
       - "doc/**"
   pull_request:
+    paths-ignore:
+      # Don't run this workflow if only files under doc/ have been
+      # modified.
+      - "doc/**"
   workflow_dispatch:
     inputs:
       LIBHTP_REPO: