Ignore zip files for docs upload diff (#7322)

This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
index 36fd3488b17f8cb0223cd70654eb0c8e4d3d4d2a..d6545473a28c3c92084ee607a146925a47dca942 100644 (file)
--- a/.github/workflows/docs_cleanup.yml
+++ b/.github/workflows/docs_cleanup.yml
@@ -1,7 +1,7 @@
 name: documentation cleanup
 on:
   schedule:
-    - cron: '0 1 * * SUN'
+    - cron: '0 1 * * *'
 
 jobs:
   docs-cleanup:

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index 5bc8e4486d00c7149b662558b8732cc0e525743c..d9e81b05edb650bb63d8f1b5263d5108c56ebc34 100644 (file)
--- a/.github/workflows/docs_upload.yml
+++ b/.github/workflows/docs_upload.yml
@@ -76,7 +76,7 @@ jobs:
             mv docs-new target/docs-$NAME-$HASH
             cd target/
 
-            if diff -r docs-master/ docs-$NAME-$HASH
+            if diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH
             then
               echo "Ignored run, documentation is the same as for current master"
             else