From 493579893ac4562360b97f97d52a7976b73fc0e2 Mon Sep 17 00:00:00 2001 From: Manuel Muth Date: Tue, 31 Jan 2023 11:28:51 +0100 Subject: [PATCH] fix ros version needed to be installed (#100) --- scripts/environment/setup.bash | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/environment/setup.bash b/scripts/environment/setup.bash index f9149a59..72320d4e 100644 --- a/scripts/environment/setup.bash +++ b/scripts/environment/setup.bash @@ -16,7 +16,8 @@ source $script_own_dir/../_RosTeamWs_Docker_Defines.bash source $script_own_dir/../_Team_Defines.bash # ros distribution name will be set in $ros_distro -check_and_set_ros_distro_and_version $1 +# RosTeamWS_WS_DOCKER_SUPPORT is set via .ros_team_ws_rc +check_and_set_ros_distro_and_version $1 $RosTeamWS_WS_DOCKER_SUPPORT ws_folder="$2" if [ "$2" == "-" ]; then