Turn off doc deploying for now.

util/deploy_docs_from_travis.sh

@@ -3,6 +3,8 @@
 set -e
 
 make gh-pages
+# TODO: This strips the syntax highlighting because the custom pygments lexer
+# isn't installed.
 
 git clone https://${GH_TOKEN}@github.com/${TRAVIS_REPO_SLUG} gh-pages-repo
 cd gh-pages-repo
@@ -11,13 +13,15 @@ git checkout gh-pages
 rm -rf *
 cp -r ../build/gh-pages/* .
 
+# TODO: Restore CNAME file that gets deleted by `rm -rf *`.
+
 git status
-ls 
+ls
 
 if ! $( git diff-index --quiet HEAD ) ; then
 	git config user.name "Travis CI"
 	git config user.email "$COMMIT_AUTHOR_EMAIL"
-	git add -A .
+	git add --all .
 	git commit -m "Deploy to GitHub Pages: ${SHA}"
-	git push 
+	git push
 fi