Make some tweaks to doc deploy script.

- Rename file to match other naming conventions.
- Simplify condition a little.

util/deploy_docs_from_travis.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+set -e
+
+make gh-pages
+
+git clone https://${GH_TOKEN}@github.com/${TRAVIS_REPO_SLUG} gh-pages-repo
+cd gh-pages-repo
+git checkout gh-pages
+
+rm -rf *
+cp -r ../build/gh-pages/* .
+
+git status
+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 commit -m "Deploy to GitHub Pages: ${SHA}"
+	git push 
+fi