projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 09c6f95) | patch
Fix inadvertent failure of workflow step (#7420)
authorGereon Kremer <nafur42@gmail.com>
Wed, 20 Oct 2021 21:42:16 +0000 (14:42 -0700)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 21:42:16 +0000 (21:42 +0000)
commit79fb4d7cb03b5fe254fb0c43f5dc6e885cfbf013
treeb048d5581d2d295df2d996302321f31d70d18c98tree
parent09c6f9514b993c78c662ff6d3f46acce97286068commit | diff
Fix inadvertent failure of workflow step (#7420)

This fixes an issue introduced with #7352: jobs fail immediately if any command has a non-zero exit code. The way we obtained the exit code of the `diff` command was incompatible with this policy, which is why we currently never upload any docs to `docs-ci`.
.github/workflows/docs_upload.yml diff | blob | history