Docs: cancel PR builds if there is no documentation changes (#9734)

* Docs: cancel PR builds if there is no documentation changes

Use the new feature to cancel builds if there are not documentation changes

* Use quotes to make the script valid

* Change logic to use $? (last exit code) in the condition

We don't have to exit the command immediately when `git diff` exists with 1;
that means there are changes and we want to continue building the documentation.

* Modify if statement

* Update docs to use the new command

* Update .readthedocs.yml

Co-authored-by: Benjamin Balder Bach <[email protected]>

Co-authored-by: Benjamin Balder Bach <[email protected]>

Author: humitos

.readthedocs.yml

@@ -14,6 +14,20 @@ build:
   os: ubuntu-22.04
   tools:
     python: "3.10"
+  jobs:
+    post_checkout:
+      # https://docs.readthedocs.io/en/stable/build-customization.html#cancel-build-based-on-a-condition
+      #
+      # Cancel building pull requests when there aren't changed in the docs directory.
+      #
+      # If there are no changes (git diff exits with 0) we force the command to return with 183.
+      # This is a special exit code on Read the Docs that will cancel the build immediately.
+      - |
+        if [ "$READTHEDOCS_VERSION_TYPE" = "external" ] && git diff --quiet origin/main -- docs/;
+        then
+          echo "No changes to docs/ - exiting the build.";
+          exit 183;
+        fi
 
 search:
   ranking:

docs/user/build-customization.rst

@@ -140,15 +140,13 @@ Here is an example that cancels builds from pull requests when there are no chan
      jobs:
        post_checkout:
          # Cancel building pull requests when there aren't changed in the docs directory.
-         # `--quiet` exits with a 1 when there **are** changes,
-         # so we invert the logic with a !
          #
-         # If there are no changes (exit 0) we force the command to return with 183.
+         # If there are no changes (git diff exits with 0) we force the command to return with 183.
          # This is a special exit code on Read the Docs that will cancel the build immediately.
          - |
-           if [ $READTHEDOCS_VERSION_TYPE = "external" ];
+           if [ "$READTHEDOCS_VERSION_TYPE" = "external" ] && git diff --quiet origin/main -- docs/;
            then
-             ! git diff --quiet origin/main -- docs/ && exit 183;
+             exit 183;
            fi