blob: 7ddae016142f73836014974cf30c7548b68d715e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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
|
