diff --git a/publish.py b/publish.py index 4013051ad..9f7398420 100755 --- a/publish.py +++ b/publish.py @@ -101,6 +101,8 @@ def run_man(args: Any) -> None: def run_html(args: Any) -> None: + # Force a fresh build otherwise the search index is not correct + shutil.rmtree(os.path.join(docs_dir, '_build', 'dirhtml')) call('make FAIL_WARN=1 "OPTS=-D analytics_id=G-XTJK3R7GF2" dirhtml', cwd=docs_dir) add_old_redirects('docs/_build/dirhtml')