diff --git a/tools/build-docs b/tools/build-docs index 44e81553f8..5b8dca523e 100755 --- a/tools/build-docs +++ b/tools/build-docs @@ -1,3 +1,22 @@ -#!/usr/bin/env bash -set -eu -make -C "$(dirname "$0")"/../docs clean html +#!/usr/bin/env python3 + +# check for the venv +from lib import sanity_check + +sanity_check.check_venv(__file__) + +import os +import sys + +ZULIP_PATH = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +sys.path.append(ZULIP_PATH) +from scripts.lib.zulip_tools import run + + +def main() -> None: + path = os.path.join(ZULIP_PATH, "docs") + run(["make", "clean", "html", "-C", path]) + + +if __name__ == "__main__": + main()