avoid spawning whoami to get username in tools/install-gnuarm4.sh

diff --git a/tools/install-gnuarm4.sh b/tools/install-gnuarm4.sh
index ffb509bfc27fbc5c73ce51e2e7b2fef4d0892153..c55d81f214540a75ea41adec5bcaf23c679f6048 100755 (executable)
--- a/tools/install-gnuarm4.sh
+++ b/tools/install-gnuarm4.sh
@@ -81,7 +81,7 @@ GPG_OPTS="--keyring ${GNU_KEYRING_GPG} --no-default-keyring --homedir ."
 # End of configuration section. You shouldn't have to modify anything below.
 ############################################################################
 
-if [[ `whoami` != "root" ]]; then
+if [[ "$USER" != "root" ]]; then
   echo "*** Warning! Not running as root!"
   echo "Installation may fail if you do not have appropriate permissions!"
 fi