From 85f005ea52535c3e93165037383285818902c54e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 16 Aug 2016 10:45:17 +0200
Subject: [PATCH] Remove old branch from gitlab-ci.yml

---
 .gitlab-ci.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f24ff612b..f06e1af5e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -10,7 +10,6 @@ buildjob:
   - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
   only:
   - master
-  - jh_simplified_resources
   artifacts:
     paths:
     - build-time.txt
-- 
GitLab