post-commit for committing docs

post-commit.sh

#!/bin/sh
#
# Deploys documentation

getGitBranchName()
{
    branch="$(git symbolic-ref HEAD 2>/dev/null)" ||
            "$(git describe --contains --all HEAD)"
    echo ${branch##refs/heads/}
}

isOnMasterBranch()
{
    if [ "$(getGitBranchName)" = "master" ]; then
        return 0
    fi
    return 1
}

isOnMasterBranch
if [ $? -ne 0 ]; then # ignore any branch *except* master
    exit
fi

make clean
make
git checkout gh-pages
git rm -r symbols
git rm -r static
git rm index.html
rm -r src
rm -r test
mv docs/* ./
rm -r docs

pushd symbols

# move src up a directory
mv src/* ./
rm -r src

# rename _global_ => global to make Jekyll happy
for i in $(find . -type f); do sed 's/_global_/global/g' $i > $i-tmp; mv $i-tmp $i; done
mv _global_.html global.html
popd

sed 's/_global_/global/g' index.html > index.html.tmp
mv index.html.tmp index.html

git add .
git commit -m "Documentation updated to reflect master"
git checkout master