diff --git a/contrib/update_docs.sh b/contrib/update_docs.sh new file mode 100755 index 000000000..f517e1e5b --- /dev/null +++ b/contrib/update_docs.sh @@ -0,0 +1,12 @@ +#/bin/bash + +cd $( cd "$( dirname "$0" )/.." && pwd ) + +LASTREV=$(git rev-parse HEAD) +git pull --all +NEWREV=$(git rev-parse HEAD) + +if [ "$LASTREV" != "$NEWREV" ]; then + echo "There's a new version. Running doxygen" + doxygen +fi