Merge pull request #5838 from maxGimeno/Fix_doc_removal-maxGimeno

Online Doc: Fix condition for push

.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