From fb741582ef205b6bece7644563bff842323a659f Mon Sep 17 00:00:00 2001
From: Florian Bruhin <git@the-compiler.org>
Date: Tue, 5 Apr 2016 12:43:51 +0200
Subject: [PATCH] scripts/dev/ci/install: Retry apt-get if it fails

---
 scripts/dev/ci/install.py | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/scripts/dev/ci/install.py b/scripts/dev/ci/install.py
index a772b5d72..b96b9f72c 100644
--- a/scripts/dev/ci/install.py
+++ b/scripts/dev/ci/install.py
@@ -69,7 +69,13 @@ def folded_cmd(argv):
 
 
 def apt_get(args):
-    folded_cmd(['sudo', 'apt-get', '-y', '-q'] + args)
+    try:
+        folded_cmd(['sudo', 'apt-get', '-y', '-q'] + args)
+    except subprocess.CalledProcessError:
+        print()
+        print("apt-get failed... trying a second time!")
+        print()
+        folded_cmd(['sudo', 'apt-get', '-y', '-q'] + args)
 
 
 def brew(args):