From a85c3189fa7f5b2a40b49ac953d88cf8c8ca8206 Mon Sep 17 00:00:00 2001 From: Erik Faye-Lund Date: Wed, 21 Oct 2020 14:00:23 +0200 Subject: [PATCH] docs: create leading directories for redirects This will be useful when removing entire directories from the docs, which will happen in an upcoming patch. Reviewed-by: Eric Anholt Part-of: --- docs/_exts/redirects.py | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/_exts/redirects.py b/docs/_exts/redirects.py index eb5d082d3b5..0320f2c21aa 100644 --- a/docs/_exts/redirects.py +++ b/docs/_exts/redirects.py @@ -15,6 +15,7 @@ def create_redirects(app, docname): return for src, dst in redirects: path = os.path.join(app.outdir, '{0}.html'.format(src)) + os.makedirs(os.path.dirname(path), exist_ok=True) with open(path, 'w') as f: f.write(create_redirect(dst))