From 8c3374398ad6bfb3ed141c749ce8d4b89e04bc1e Mon Sep 17 00:00:00 2001
From: Ian McInerney <ian.s.mcinerney@ieee.org>
Date: Sun, 17 May 2020 00:08:25 +0100
Subject: [PATCH] Don't interrupt compilation pipelines

Don't interrupt the compilation pipelines, instead let
them finish. That will ensure the author of the change
gets notified if their push breaks something.
---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a159b1eaa6..6a196ab7a9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -79,7 +79,7 @@ test_formatting:
 build_linux:
   stage: build
   extends: .only_code
-  interruptible: true
+  interruptible: false
   cache:
     key: "cache-linux"
     paths: