[docs] improve redirects destination

This commit is contained in:
Ivan Blinkov 2020-07-06 12:56:30 +03:00 committed by GitHub
parent 5c6d6bdf54
commit 9e776e6907
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -169,7 +169,8 @@ def build_docs(args):
if lang:
tasks.append((lang, args,))
util.run_function_in_parallel(build_for_lang, tasks, threads=False)
redirects.build_docs_redirects(args)
if not args.version_prefix:
redirects.build_docs_redirects(args)
def build(args):