# This script performs continued docs updating.
#
# This will continuously rebuild the documentation (about once every 30 seconds
# in practice) and automatically reloads the page in the browser.
#
# The documentation from the `bp` command line utility does not get rebuilt this
# way: use scripts/make_bp_help_documentation

pushd doc
make livehtml
popd
