tools/fetch-distro: only fetch the configured branch
authorZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
Wed, 3 Jul 2024 14:10:49 +0000 (16:10 +0200)
committerZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
Mon, 22 Jul 2024 09:38:08 +0000 (11:38 +0200)
commit8e84e154457b0d55e823f670c377233b0211d2b7
tree9d8c5c05bd6e49699cc6e4492db592dc558b6adf
parent82c459f910c3036b22c9f41472b622ef4bfdab1d
tools/fetch-distro: only fetch the configured branch

We don't need the other branches. This mostly cuts down on the
noise in output. But add '-v' to show what we're fetching.
tools/fetch-distro.py