diff options
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/build-otp | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/scripts/build-otp b/scripts/build-otp index abdffe8759..e33bf95286 100755 --- a/scripts/build-otp +++ b/scripts/build-otp @@ -57,23 +57,23 @@ if [ "$1" = "docs" ]; then do_and_log "Linting documentation" make xmllint # The code below prepares this build to be used as a deploy to # github pages for documentation. - if [ "$TRAVIS_PULL_REQUEST" = "false" -a "$TRAVIS_TAG" = "" ]; then - set -x - rm -rf logs - SHA=`git rev-parse --verify HEAD` - DATE=`date -Iseconds` - git clean -xfdq -e $DOC_TARGET - git fetch https://github.com/$TRAVIS_REPO_SLUG gh-pages - git checkout -f FETCH_HEAD - rm -rf _docs/$DOC_TARGET - mv $DOC_TARGET _docs/$DOC_TARGET - echo "---" > _docs/$DOC_TARGET.md - echo "title: $DOC_TARGET" >> _docs/$DOC_TARGET.md - echo "sha: $SHA" >> _docs/$DOC_TARGET.md - echo "generated: $DATE" >> _docs/$DOC_TARGET.md - echo "---" >> _docs/$DOC_TARGET.md - set +x - fi + # if [ "$TRAVIS_PULL_REQUEST" = "false" -a "$TRAVIS_TAG" = "" ]; then + # set -x + # rm -rf logs + # SHA=`git rev-parse --verify HEAD` + # DATE=`date -Iseconds` + # git clean -xfdq -e $DOC_TARGET + # git fetch https://github.com/$TRAVIS_REPO_SLUG gh-pages + # git checkout -f FETCH_HEAD + # rm -rf _docs/$DOC_TARGET + # mv $DOC_TARGET _docs/$DOC_TARGET + # echo "---" > _docs/$DOC_TARGET.md + # echo "title: $DOC_TARGET" >> _docs/$DOC_TARGET.md + # echo "sha: $SHA" >> _docs/$DOC_TARGET.md + # echo "generated: $DATE" >> _docs/$DOC_TARGET.md + # echo "---" >> _docs/$DOC_TARGET.md + # set +x + # fi fi exit 0 |