From 601b23a59fbc60cd047522598db702ce44cf7f0a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 8 Oct 2021 04:02:51 -0700 Subject: [PATCH] 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. --- .github/workflows/docs_cleanup.yml | 2 +- .github/workflows/docs_upload.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 -- 2.30.2