Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix documentation workflow always trying to commit
Don't try to commit and push if there is nothing to commit, because git will exit with 1, failing the workflow. A continuation of ca6b87d.
- Loading branch information