From aadf6f68289f8ec1042c45b3e29610c2da786150 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 1 Mar 2018 17:38:06 +0100
Subject: build: win: detect 404 as HTML files

---
 dev/build/windows/makecoq_mingw.sh | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 17a94accd8..4c99648c3a 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
-- 
cgit v1.2.3