diff options
Diffstat (limited to 'doc/gh-pages.sh')
| -rw-r--r-- | doc/gh-pages.sh | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/doc/gh-pages.sh b/doc/gh-pages.sh deleted file mode 100644 index 9a5bcec..0000000 --- a/doc/gh-pages.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh -set -e - -REV=$(git rev-parse HEAD) - -cd "$(dirname "$0")" -git stash -dune build @doc -git checkout gh-pages -rm -rf doc -cp -R _build/default/_doc/_html doc -git add doc -git commit -m "Update documentation for $REV" -git checkout master -git stash apply |