diff options
| author | dequis <dx@dxzone.com.ar> | 2017-07-09 00:10:53 -0300 |
|---|---|---|
| committer | dequis <dx@dxzone.com.ar> | 2017-07-09 00:10:53 -0300 |
| commit | 4d51c8451c6abb2fa90e099034fcc9c39e7530aa (patch) | |
| tree | 1fd49346566068c5319f0d784cc1b12bd553610b | |
| parent | b9c10a1afa791d531c70df88874d07f34b26eb90 (diff) | |
configure: Don't require python if docs are already built
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -769,7 +769,7 @@ fi if [ "$doc" = "1" ]; then # check this here just in case someone tries to install it in python2.4... - if ! $PYTHON -m xml.etree.ElementTree > /dev/null 2>&1; then + if [ ! -e $srcdir/doc/user-guide/help.txt ] && ! $PYTHON -m xml.etree.ElementTree > /dev/null 2>&1; then echo echo 'ERROR: Python (>=2.5 or 3.x) is required to generate docs' echo "(Use the PYTHON environment variable if it's in a weird location)" |