Merge pull request #5446 from maxGimeno/diff

Fix CI doc deletion
2021-03-10 10:33:12 +01:00 · 2021-03-10 10:33:12 +01:00 · 39339adbcc
parent fe81fced45 7161686c46
commit 39339adbcc
1 changed files with 1 additions and 1 deletions
--- a/.github/workflows/delete_doc.yml
+++ b/.github/workflows/delete_doc.yml
@ -26,7 +26,7 @@ jobs:
           git rm -r ${PR_NUMBER} 
         fi
         #git diff exits with 1 if there is a diff
-         if !git diff --quiet; then
+         if ! git diff --quiet; then
           git commit -a --amend -m"base commit" && git push -f -u origin master
         fi