Fix condition for push

2021-07-07 15:10:09 +02:00 · 2021-07-07 15:10:09 +02:00 · 9e29edb42c
parent e4f1530590
commit 9e29edb42c
1 changed files with 2 additions and 2 deletions
--- a/.github/workflows/delete_doc.yml
+++ b/.github/workflows/delete_doc.yml
@ -25,8 +25,8 @@ jobs:
         if [ -d ${PR_NUMBER} ]; then 
           git rm -r ${PR_NUMBER} 
         fi
-         #git diff exits with 1 if there is a diff
-         if ! git diff --quiet; then
+         #git diff exits with 1 if there is no diff
+         if  git diff --quiet; then
           git commit -a --amend -m"base commit" && git push -f -u origin master
         fi