From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 8 Oct 2021 11:02:51 +0000 (-0700)
Subject: Ignore zip files for docs upload diff (#7322)
X-Git-Tag: cvc5-1.0.0~1101
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=601b23a59fbc60cd047522598db702ce44cf7f0a;p=cvc5.git

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 36fd3488b..d6545473a 100644
--- 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 5bc8e4486..d9e81b05e 100644
--- 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