Re: [PATCH v3 4/5] CI: use "$runs_on_pool", not "$jobname" to select packages & config

Ævar Arnfjörð Bjarmason  [off-list ref] writes:

-case "$jobname" in
-linux-clang|linux-gcc|linux-leaks)
+case "$runs_on_pool" in
+ubuntu-latest)
 	sudo apt-get -q update
...
 	;;
-osx-clang|osx-gcc)
+macos-latest)
 	export HOMEBREW_NO_AUTO_UPDATE=1 HOMEBREW_NO_INSTALL_CLEANUP=1

Indeed this is nice improvement in maintainability.