doc/gh-pages.sh


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

#!/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