diff --git a/.gitignore b/.gitignore index 359907e8..05cdd11f 100644 --- a/.gitignore +++ b/.gitignore @@ -36,3 +36,4 @@ TAGS build* +gh-pages diff --git a/etc/deploy-doc.sh b/etc/deploy-doc.sh new file mode 100755 index 00000000..09496ef4 --- /dev/null +++ b/etc/deploy-doc.sh @@ -0,0 +1,28 @@ +#!/bin/bash +set -e + +if ! [[ -d "gh-pages" ]] ; then + echo -e "Error, the \"gh-pages\" directory is not present:" + echo -e "git clone --branch=gh-pages git@github.com:libsemigroups/hpcombi.git gh-pages" + exit 1 +fi + +printf "\033[0;32mDeploying updates to GitHub...\033[0m\n" + +mkdir -p build +cd build +if [[ -f Makefile ]] ; then + make clean +fi +cmake .. +make doc +cd .. +cp -r build/doc/html/* gh-pages +cd gh-pages +git add . +msg="rebuilding site $(date)" +if [ -n "$*" ]; then + msg="$*" +fi +git commit -m "$msg" +# git push origin gh-pages