From 14334dce21f584a60fcc8214996ae28c86df7ffe Mon Sep 17 00:00:00 2001
From: Florian Bruhin <git@the-compiler.org>
Date: Fri, 23 Oct 2015 08:10:15 +0200
Subject: [PATCH] Don't remove coverage.xml on CI.

---
 scripts/dev/check_coverage.py | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/scripts/dev/check_coverage.py b/scripts/dev/check_coverage.py
index b1c1f2cdb..65228a10e 100644
--- a/scripts/dev/check_coverage.py
+++ b/scripts/dev/check_coverage.py
@@ -203,7 +203,10 @@ def main_check():
     for msg in messages:
         print(msg.text)
 
-    os.remove('coverage.xml')
+    if 'CI' in os.environ:
+        print("Keeping coverage.xml on CI.")
+    else:
+        os.remove('coverage.xml')
     return 1 if messages else 0