From f0d47ab88ef18d64de234c49c89caecdbfd906ea Mon Sep 17 00:00:00 2001
From: Pietro Incardona <incardon@mpi-cbg.de>
Date: Sat, 16 May 2020 23:19:50 +0200
Subject: [PATCH] Defete broken VCDEVEL

---
 script/install_VCDEVEL.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/script/install_VCDEVEL.sh b/script/install_VCDEVEL.sh
index 9c6d05be5..671db9442 100755
--- a/script/install_VCDEVEL.sh
+++ b/script/install_VCDEVEL.sh
@@ -2,7 +2,7 @@
 
 # check if the directory $1/VCDEVEL exist
 
-if [ -d "$1/VCDEVEL" ]; then
+if [ -d "$1/VCDEVEL" && -f "$1/VCDEVEL/include/Vc/Vc" ]; then
   echo "VCDEVEL already installed"
   exit 0
 fi
-- 
GitLab