diff --git a/.github/setup_ci.sh b/.github/setup_ci.sh index 658803457229..6d0da53527c6 100755 --- a/.github/setup_ci.sh +++ b/.github/setup_ci.sh @@ -272,6 +272,7 @@ if [ ! -z "${INSTALL_PUTTY}" ]; then fi if [ "${TARGET}" = "tcsh" ]; then + id echo "Setting $(whoami) login shell to /usr/bin/tcsh" sudo chsh -s /usr/bin/tcsh $(whoami) grep $(whoami) /etc/passwd