diff --git a/docs/build_docs.py b/docs/build_docs.py index 877179bd33..9dc902f69c 100755 --- a/docs/build_docs.py +++ b/docs/build_docs.py @@ -161,8 +161,7 @@ def sphinx_call(language, target, build_dir, sphinx_parallel_jobs, buildername): try: os.makedirs(build_dir) except OSError: - print("Cannot call Sphinx in an existing directory!") - return 1 + pass environ = {} environ.update(os.environ)