Ignore zip files for docs upload diff (#7322)
[cvc5.git] / .github / workflows / docs_upload.yml
index 5bc8e4486d00c7149b662558b8732cc0e525743c..d9e81b05edb650bb63d8f1b5263d5108c56ebc34 100644 (file)
@@ -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