diff --git a/dist/tools/ci/print_toolchain_versions.sh b/dist/tools/ci/print_toolchain_versions.sh index 7aa2f6480c..dbb0993ad9 100755 --- a/dist/tools/ci/print_toolchain_versions.sh +++ b/dist/tools/ci/print_toolchain_versions.sh @@ -8,6 +8,10 @@ get_cmd_version() { local cmd="$1" if command -v "$cmd" 2>&1 >/dev/null; then ver=$("$cmd" --version 2> /dev/null | head -n 1) + # some tools (eg. openocd) print version info to stderr + if [ -z "$ver" ]; then + ver=$("$cmd" --version 2>&1 | head -n 1) + fi if [ -z "$ver" ]; then ver="error" fi