From e01958273883068f0595682a3ada629933caba2a Mon Sep 17 00:00:00 2001
From: Simon <oehrl@vr.rwth-aachen.de>
Date: Wed, 15 Jan 2020 16:20:20 +0100
Subject: [PATCH] Fix plugin detection
---
setup.sh | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/setup.sh b/setup.sh
index 12de8b71..79ef449f 100644
--- a/setup.sh
+++ b/setup.sh
@@ -201,12 +201,12 @@ function manage_plugins() {
# Check if plugin is already present
repo_name_with_extension=${plugin_repositories[$i]##*/}
repo_name=${repo_name_with_extension%*.git}
- path=$(git config -f .gitmodules --get "submodule.Plugins/${repo_name}.path")
+ path=$(git config -f ../.gitmodules --get "submodule.Plugins/${repo_name}.path")
if [ $? -ne 0 ]
then
- plugin_present=true
- else
plugin_present=false
+ else
+ plugin_present=true
fi
if [ -n "${plugin_branches[$i]}" ]
@@ -240,6 +240,8 @@ function manage_plugins() {
fi
done
cd ..
+ echo "Done, Press enter to continue."
+ read x
fi
}
--
GitLab