diff --git a/tools/download_file.py b/tools/download_file.py index 90222c68d8..901387d2f9 100755 --- a/tools/download_file.py +++ b/tools/download_file.py @@ -7,6 +7,7 @@ import argparse import os import sys +import time try: from urllib2 import HTTPError, URLError, urlopen