2016-02-23 21:35:25 +00:00
|
|
|
#!/usr/bin/env bash
|
|
|
|
|
|
|
|
set -e
|
|
|
|
|
2016-02-24 10:46:57 +00:00
|
|
|
BRANCH_NAME=$(git branch | grep '*' | sed 's/* //')
|
|
|
|
|
|
|
|
if [[ $BRANCH_NAME == 'master' ]]; then
|
2016-02-24 10:26:05 +00:00
|
|
|
# Build new web documentation:
|
|
|
|
make build-gh-pages
|
|
|
|
fi
|