diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-08 04:02:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-08 11:02:51 +0000 |
| commit | 601b23a59fbc60cd047522598db702ce44cf7f0a (patch) | |
| tree | 6239c31499c52f04c4443b5c7ff09e2cbc5a0eb3 /.github | |
| parent | 120cc0d2283d4e629ac264d8d2c1d3ff1654be52 (diff) | |
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.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs_cleanup.yml | 2 | ||||
| -rw-r--r-- | .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 |