From 013365d6c83ae218e9972f036996c4eaf27caf70 Mon Sep 17 00:00:00 2001 From: Matthias Grob Date: Wed, 15 Feb 2023 09:01:55 +0100 Subject: [PATCH] ubuntu.sh: source the .profile after changing it such that the arm toolchain is available in that terminal without relogin for convenience. --- Tools/setup/ubuntu.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/Tools/setup/ubuntu.sh b/Tools/setup/ubuntu.sh index a823d9936d..d3f637a6a3 100755 --- a/Tools/setup/ubuntu.sh +++ b/Tools/setup/ubuntu.sh @@ -183,6 +183,7 @@ if [[ $INSTALL_NUTTX == "true" ]]; then echo "${NUTTX_GCC_VERSION} path already set."; else echo $exportline >> $HOME/.profile; + source $HOME/.profile; # Allows to directly build NuttX targets in the same terminal fi fi fi