From 2970bbdf6fa565d6e15840774f2f8145f9fc9039 Mon Sep 17 00:00:00 2001 From: Kovid Goyal Date: Mon, 5 Oct 2020 20:04:32 +0530 Subject: [PATCH] Update GA tags Also auto gen docs if running publish only for website --- publish.py | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) 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()