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

(cherry picked from commit 3658d502fff9fb981d670aa79956a0f26e3cab2c)

diff --git a/.github/workflows/builds.yml b/.github/workflows/builds.yml
index 9e695df3792190889598e82b8d7ba169b7283452..155ecc12b7f082310f42ed24d119a0a57884a717 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: