diff options
| -rwxr-xr-x | scripts/sphinx-pre-install | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/scripts/sphinx-pre-install b/scripts/sphinx-pre-install index ad9945ccb0cf..2a311ed00179 100755 --- a/scripts/sphinx-pre-install +++ b/scripts/sphinx-pre-install @@ -245,6 +245,10 @@ sub check_missing_tex($) sub get_sphinx_fname() { + if ($ENV{'SPHINXBUILD'}) { + return $ENV{'SPHINXBUILD'}; + } + my $fname = "sphinx-build"; return $fname if findprog($fname); |