From 97fee747e434e98845bab59a77680621fba031c1 Mon Sep 17 00:00:00 2001
From: Oliver Behnke <oliver.behnke@aei.mpg.de>
Date: Thu, 5 Mar 2020 20:08:02 +0100
Subject: [PATCH] List all required tools if one's missing (to ease the pain)
---
build.sh | 1 +
1 file changed, 1 insertion(+)
diff --git a/build.sh b/build.sh
index 900523f..3ce7fe8 100755
--- a/build.sh
+++ b/build.sh
@@ -155,6 +155,7 @@ check_prerequisites()
for tool in $TOOLS; do
if ! ( type $tool >/dev/null 2>&1 ); then
echo "Missing \"$tool\" which is a required tool!" | tee -a $LOGFILE
+ echo "Required are: $TOOLS" | tee -a $LOGFILE
return 1
fi
done
--
GitLab