From 8a954086738843036bbe45529060cd22ab5c3008 Mon Sep 17 00:00:00 2001 From: Gunnar Beutner Date: Wed, 21 Apr 2021 22:50:59 +0200 Subject: [PATCH] Ports: Rename dirname to port to clarify its meaning --- Ports/build_all.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Ports/build_all.sh b/Ports/build_all.sh index 3255b5f2df..4eedfbc6f8 100755 --- a/Ports/build_all.sh +++ b/Ports/build_all.sh @@ -30,7 +30,7 @@ some_failed=false for file in *; do if [ -d $file ]; then pushd $file > /dev/null - dirname=$(basename $file) + port=$(basename $file) if [ "$clean" == true ]; then if [ "$verbose" == true ]; then ./package.sh clean_all @@ -40,16 +40,16 @@ for file in *; do fi if [ "$verbose" == true ]; then if ./package.sh; then - echo "Built ${dirname}." + echo "Built ${port}." else - echo "ERROR: Build of ${dirname} was not successful!" + echo "ERROR: Build of ${port} was not successful!" some_failed=true fi else if ./package.sh > /dev/null 2>&1; then - echo "Built ${dirname}." + echo "Built ${port}." else - echo "ERROR: Build of ${dirname} was not successful!" + echo "ERROR: Build of ${port} was not successful!" some_failed=true fi fi