m/grafX2
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

3rdparty: improve curl output. make it save file timestamp (as wget does)

Browse Source
This commit is contained in:
Thomas Bernard 2019-01-25 21:56:17 +01:00
parent 41b857c739
commit c9b0907151
No known key found for this signature in database
GPG Key ID: 0FF11B67A5C0863C
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
3rdparty/Makefile vendored
View File

@ -76,7 +76,7 @@ TAR = $(shell which tar)
# wget -nv option is used to avoid messing the output when using "make -j3" # wget -nv option is used to avoid messing the output when using "make -j3"
GETURL = $(shell WGET=`which wget` ; if [ "$$?" = "0" ] && [ -x "$$WGET" ] ; \ GETURL = $(shell WGET=`which wget` ; if [ "$$?" = "0" ] && [ -x "$$WGET" ] ; \
then echo "$$WGET -nv" ; \ then echo "$$WGET -nv" ; \
else echo "curl -O -L --max-time 120" ; fi ) else echo 'curl -s -w "%{url_effective} downloaded to %{filename_effective} in %{time_total} seconds\\n" -R -O -L --max-time 120' ; fi )
BUILD_CC := $(CC) BUILD_CC := $(CC)
STRIP = strip STRIP = strip