Juan Carrano 02b72ab385 print_toolchain_versions: print system and make's default shell. ... Some systems use dash as system shell, others use bash. The shell used by make can also be different, and unrelated to the system shell. Differences in this variable can cause problems when testing PRs and reporting bugs. The default shell is important system information that should be reported.		2020-01-07 09:28:46 +01:00
..
build_and_test.sh	tools/ci: fix typo in build_and_test.sh script	2019-10-10 15:48:18 +02:00
changed_files.sh	make: Ignore checking all vendor files	2018-05-29 15:21:44 -07:00
print_toolchain_versions.sh	print_toolchain_versions: print system and make's default shell.	2020-01-07 09:28:46 +01:00