@ -2,7 +2,5 @@
set -e
# unset GIT_WORK_TREE
# Build new web documentation:
make build-gh-pages
@ -9,3 +9,4 @@ make test
# Build new manuals:
make build-man
git add man/