ci: Early exit for doc changes

.github/workflows/build-and-test.yml

@@ -1,4 +1,4 @@
-name: GitHub Actions
+name: GitHub Actions (Build)
 
 on: 
   push: 
@@ -19,6 +19,7 @@ jobs:
       env:
         GH_YML_JOBNAME: ${{ matrix.jobname }}
         GH_YML_OS: Linux
+        GH_SHA_BEFORE: ${{ github.event.before }}
 
     strategy:
       fail-fast: false
@@ -73,6 +74,7 @@ jobs:
       env:
         GH_YML_JOBNAME: ${{ matrix.jobname }}
         GH_YML_OS: Linux
+        GH_SHA_BEFORE: ${{ github.event.before }}
 
     strategy:
       fail-fast: false
@@ -117,6 +119,7 @@ jobs:
       env:
         GH_YML_JOBNAME: ${{ matrix.jobname }}
         GH_YML_OS: Linux
+        GH_SHA_BEFORE: ${{ github.event.before }}
 
     strategy:
       fail-fast: false

.github/workflows/formatting.yml

@@ -1,4 +1,4 @@
-name: Formatting
+name: GitHub Actions (Formatting)
 
 on: 
   push: 

scripts/ci/gh-actions/run.sh

@@ -1,5 +1,7 @@
 #!/bin/bash --login
 
+#set -x
+
 if [[ "${GITHUB_JOB}" =~ emu ]]
 then
   export CI_SITE_NAME="GitHub Actions (QEMU)"
@@ -82,6 +84,25 @@ echo "**********Env Begin**********"
 env | sort
 echo "**********Env End************"
 
+echo "**********Doc Check Begin************"
+if [ "${GITHUB_EVENT_NAME}" = "pull_request" ]
+then
+  git fetch origin ${GITHUB_BASE_REF}
+  REF0=$(git merge-base origin/${GITHUB_BASE_REF} HEAD)
+else
+  REF0=${GH_SHA_BEFORE}
+fi
+NFILES=$(git diff --name-only ${REF0}..HEAD | wc -l)
+NNOTDOCS=$(git diff --name-only ${REF0}..HEAD | grep -v '^docs/' | wc -l)
+echo "${NFILES} files changed, ${NNOTDOCS} not in docs/."
+git diff --name-only ${REF0}..HEAD
+if [ ${NFILES} -ne 0 -a ${NNOTDOCS} -eq 0 ]
+then
+  echo "Only changes in docs/; skipping all other CI actions."
+  exit 0
+fi
+echo "**********Doc Check End**************"
+
 echo "**********CTest Begin**********"
 ${CTEST} --version
 echo ${CTEST} -VV -S ${CTEST_SCRIPT} -Ddashboard_full=OFF ${CTEST_STEP_ARGS}