projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 437405d)
Avoid uploading docs if they did not change (#6621)
authorGereon Kremer <nafur42@gmail.com>
Thu, 27 May 2021 07:38:12 +0000 (09:38 +0200)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 07:38:12 +0000 (07:38 +0000)
Fixes an oversight from #6601.

.github/workflows/docs_upload.yml patch | blob | history

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index 7346371e3bdfc603dbdcd3fa4f221260b241681b..5bc8e4486d00c7149b662558b8732cc0e525743c 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 target/docs-master/ target/docs-$NAME-$HASH
+            if diff -r docs-master/ docs-$NAME-$HASH
             then
               echo "Ignored run, documentation is the same as for current master"
             else