| git commit-tree $$(git write-tree --prefix=Documentation) \
-p refs/heads/man) && \
rm -f $${GIT_INDEX_FILE} && \
git add -f Documentation/*.html && \
git update-ref refs/heads/html \
| git commit-tree $$(git write-tree --prefix=Documentation) \
-p refs/heads/man) && \
rm -f $${GIT_INDEX_FILE} && \
git add -f Documentation/*.html && \
git update-ref refs/heads/html \