projects
/
cvc5.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Ignore zip files for docs upload diff (#7322)
[cvc5.git]
/
.github
/
workflows
/
docs_upload.yml
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