[gimp-web/wip/Jehan/fix-ci: 11/11] tools: try adding headers again to the requests.get() call.

[Jehan <jehanp src gnome org>]

commit 265184cd16bed84ec6de3dac0a155e1a59bfa3fb
Author: Jehan <jehan girinstud io>
Date:   Mon May 2 16:26:37 2022 +0200

    tools: try adding headers again to the requests.get() call.
    
    Similar to the previous change when I was using urllib.request API.

 tools/downloads/gimp-check-mirrors.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)
---
diff --git a/tools/downloads/gimp-check-mirrors.py b/tools/downloads/gimp-check-mirrors.py
index 1d5964c8..1559536c 100755
--- a/tools/downloads/gimp-check-mirrors.py
+++ b/tools/downloads/gimp-check-mirrors.py
@@ -99,7 +99,8 @@ def verify_remote(uri, future):
   checksum_ok = None
   try:
     if future is not None:
-      with requests.get(uri, stream=True) as response:
+      headers = {'user-agent': 'Mozilla/5.0'}
+      with requests.get(uri, headers=headers, stream=True) as response:
         m = hashlib.sha256()
         # I don't think the chunk_size is useful, since docs
         # says that "stream=True will read data as it arrives