github-repos/wget
1
0
Fork 0
mirror of https://github.com/mirror/wget.git synced 2025-03-29 13:30:30 +08:00
Code Issues Packages Projects Releases Wiki Activity

* bootstrap: Use the faster gnulib-tool.py script if possible

Browse Source
This commit is contained in:
Darshit Shah 2018-01-14 11:33:52 +01:00
parent 953bcdaba8
commit b1fc37f465
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
bootstrap
View File

@ -688,8 +688,11 @@ if $bootstrap_sync; then
} }
fi fi
gnulib_tool=$GNULIB_SRCDIR/gnulib-tool gnulib_tool=$GNULIB_SRCDIR/gnulib-tool.py
<$gnulib_tool || exit $? if ! <$gnulib_tool; then
gnulib_tool=$GNULIB_SRCDIR/gnulib-tool
<$gnulib_tool || exit $?
fi
# Get translations. # Get translations.