projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 120cc0d) | patch
Ignore zip files for docs upload diff (#7322)
authorGereon Kremer <nafur42@gmail.com>
Fri, 8 Oct 2021 11:02:51 +0000 (04:02 -0700)
committerGitHub <noreply@github.com>
Fri, 8 Oct 2021 11:02:51 +0000 (11:02 +0000)
commit601b23a59fbc60cd047522598db702ce44cf7f0a
tree6239c31499c52f04c4443b5c7ff09e2cbc5a0eb3tree
parent120cc0d2283d4e629ac264d8d2c1d3ff1654be52commit | 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.
.github/workflows/docs_cleanup.yml diff | blob | history
.github/workflows/docs_upload.yml diff | blob | history