diff --git a/publish.py b/publish.py index e14af0703..3691a2231 100755 --- a/publish.py +++ b/publish.py @@ -68,14 +68,15 @@ def run_html(args: Any) -> None: def add_analytics() -> None: analytics = ''' - + + - -\ ''' for dirpath, firnames, filenames in os.walk(publish_dir): for fname in filenames: @@ -87,6 +88,10 @@ ga('send', 'pageview'); f.write(html.encode('utf-8')) +def run_docs(args: Any) -> None: + subprocess.check_call(['make', 'docs']) + + def run_website(args: Any) -> None: if os.path.exists(publish_dir): shutil.rmtree(publish_dir) @@ -384,6 +389,8 @@ def main() -> None: ans = 'n' if ans.lower() != 'y': return + if actions == ['website']: + actions.insert(0, 'docs') for action in actions: print('Running', action) cwd = os.getcwd()