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