diff --git a/tools/pushdocs b/tools/pushdocs new file mode 100755 index 000000000..c3a065bb2 --- /dev/null +++ b/tools/pushdocs @@ -0,0 +1,23 @@ +#!/usr/bin/env bash +# PROG MSG - commit manuals with ";doc: MSG" prefix, push to CI, then to master + +set -e + +DELAY=30 +INTERVAL=10 +MSG=";doc: $1" + +#WAIT="sleep $DELAY" +WAIT="ciwatch $INTERVAL" + +git commit -uno -m "$MSG" hledger/hledger.m4.md hledger-ui/hledger-ui.m4.md hledger-web/hledger-web.m4.md || true +git push -f github master:simon \ +&& echo "waiting for CI to finish..." \ +&& $WAIT \ +&& git push github master \ +&& printf "Docs should be up to date momentarily:\n\ +\n\ +https://hledger.org/dev/hledger.html\n\ +https://hledger.org/dev/hledger-ui.html\n\ +https://hledger.org/dev/hledger-web.html\n\ +"