diff options
Diffstat (limited to 'tool/update-gh-pages')
-rwxr-xr-x | tool/update-gh-pages | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/tool/update-gh-pages b/tool/update-gh-pages deleted file mode 100755 index 8eb546a9..00000000 --- a/tool/update-gh-pages +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/sh -set -e - -# Generates RDoc HTML and update gh-pages branch. - -HEAD_DESCRIPTION=$(git describe --dirty --always --abbrev=12) - -[ -d html ] && - rm -r html -rake rdoc - -[ ! -d tmp/gh-pages ] && - git worktree add tmp/gh-pages gh-pages -( - cd tmp/gh-pages - - git rm -r . - cp -r ../../html/* . - rm created.rid js/*.gz # to avoid unnecessary change :x - git add . - git commit -m "Sync with $HEAD_DESCRIPTION" -) |