On 10/08/20 21:06, Paolo Bonzini wrote: >>> diff --git a/configure b/configure >>> index 21b9ed2..7e7b4d8 100755 >>> --- a/configure >>> +++ b/configure >>> @@ -7768,7 +7768,6 @@ echo "INSTALL_PROG=$install -c -m 0755" >> >>> $config_host_mak >>> echo "INSTALL_LIB=$install -c -m 0644" >> $config_host_mak >>> echo "PYTHON=$python" >> $config_host_mak >>> echo "SPHINX_BUILD=$sphinx_build" >> $config_host_mak >>> -echo "SPHINX_WERROR=$sphinx_werror" >> $config_host_mak >> Shouldn't we also be deleting the code in configure that >> sets $sphinx_werror if we're no longer using it ? > Yes. >
... It's still used by has_sphinx_build, actually. Paolo
