From 6b27bd8e8fc25ee5bb91743f5ac99a7f4fa85032 Mon Sep 17 00:00:00 2001
From: Pietro Incardona <incardon@mpi-cbg.de>
Date: Thu, 23 Jul 2020 23:43:21 +0200
Subject: [PATCH] Fixing devtool-7

---
 build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.sh b/build.sh
index 8e7cb2f43..27580430a 100755
--- a/build.sh
+++ b/build.sh
@@ -23,7 +23,7 @@ echo "GPU compilation: $with_gpu"
 
 if [ x"$hostname" == x"cifarm-centos-node.mpi-cbg.de"  ]; then
 	echo "CentOS node"
-	scl enable "devtoolset-7"
+	scl enable devtoolset-7 bash
 fi
 
 if [ x"$hostname" == x"cifarm-ubuntu-node"  ]; then
-- 
GitLab