diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-01 17:38:06 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-02 08:52:37 +0100 |
| commit | aadf6f68289f8ec1042c45b3e29610c2da786150 (patch) | |
| tree | d79a6440fce1d49df375ad8636c4166a5c012927 /dev/build | |
| parent | 2dd05518ade9f19161eb0699db5e5ece34ca29d4 (diff) | |
build: win: detect 404 as HTML files
Diffstat (limited to 'dev/build')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 17a94accd..4c99648c3 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -223,6 +223,12 @@ function get_expand_source_tar { cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS else wget $1/$2.$3 + if file -i $2.$3 | grep text/html; then + echo Download failed: $1/$2.$3 + echo The file wget downloaded is an html file: + cat $2.$3 + exit 1 + fi if [ ! "$2.$3" == "$name.$3" ] ; then mv $2.$3 $name.$3 fi |