From 74853ead74c7d8c5033e25b08516985bd09ccd03 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20M=C3=B6bius?= <moebius@cs.rwth-aachen.de>
Date: Wed, 11 Nov 2015 14:34:33 +0100
Subject: [PATCH] Removed unnacessary line

---
 CI/ci-linux.sh | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CI/ci-linux.sh b/CI/ci-linux.sh
index 7af6bdee..30a08372 100755
--- a/CI/ci-linux.sh
+++ b/CI/ci-linux.sh
@@ -3,8 +3,6 @@
 COMPILER=$1
 LANGUAGE=$2
 
-#!/bin/bash
-
 OPTIONS=""
 
 if [ "$COMPILER" == "gcc" ]; then