diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/pushdoc.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh index ddab752..bea97f0 100644 --- a/scripts/pushdoc.sh +++ b/scripts/pushdoc.sh | |||
| @@ -19,6 +19,7 @@ git commit -m "Deploy to GitHub Pages" | |||
| 19 | # repo's gh-pages branch. (All previous history on the gh-pages branch | 19 | # repo's gh-pages branch. (All previous history on the gh-pages branch |
| 20 | # will be lost, since we are overwriting it.) We redirect any output to | 20 | # will be lost, since we are overwriting it.) We redirect any output to |
| 21 | # /dev/null to hide any sensitive credential data that might otherwise be exposed. | 21 | # /dev/null to hide any sensitive credential data that might otherwise be exposed. |
| 22 | echo "Pushing haddock to gh-pages" | ||
| 22 | git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1 | 23 | git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1 |
| 23 | 24 | ||
| 24 | popd | 25 | popd |