diff options
author | Matthias P. Braendli <matthias.braendli@mpb.li> | 2015-12-31 11:30:53 +0100 |
---|---|---|
committer | Matthias P. Braendli <matthias.braendli@mpb.li> | 2015-12-31 11:30:53 +0100 |
commit | e00bc13e49a2f990cb70171ac8d2b5279a77adbd (patch) | |
tree | 51346280ba197409529069d52d17e2e1d19ec600 /.travis-deploy.sh | |
parent | ef90c9ccf9cee7913b759f69da48e59e8d4161e0 (diff) | |
download | mmbtools-doc-e00bc13e49a2f990cb70171ac8d2b5279a77adbd.tar.gz mmbtools-doc-e00bc13e49a2f990cb70171ac8d2b5279a77adbd.tar.bz2 mmbtools-doc-e00bc13e49a2f990cb70171ac8d2b5279a77adbd.zip |
Add deployment to gh-pages
Diffstat (limited to '.travis-deploy.sh')
-rw-r--r-- | .travis-deploy.sh | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/.travis-deploy.sh b/.travis-deploy.sh new file mode 100644 index 0000000..7ddae01 --- /dev/null +++ b/.travis-deploy.sh @@ -0,0 +1,28 @@ +#!/bin/bash +# +# This script is called by Travis-CI to deploy +# to github pages + +set -e + +# clear and re-create the out directory +rm -rf out || exit 0; +mkdir out + +# copy all output files to the out directory +cp mmbtools.pdf out/ + +# go to the out directory and create a *new* Git repo +cd out +git init + +git config user.name "Travis CI" +git config user.email "Travis-CI@opendigitalradio.org" +git add . +git commit -m "Deploy to GitHub Pages" + +# Force push from the current repo's master branch to the remote +# repo's gh-pages branch. (All previous history on the gh-pages branch +# will be lost, since we are overwriting it.) We redirect any output to +# /dev/null to hide any sensitive credential data that might otherwise be exposed. +git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1 |