bin/get-extra-pick-list: rework to use already_picked list
authorEmil Velikov <emil.velikov@collabora.com>
Sat, 11 Feb 2017 12:45:21 +0000 (12:45 +0000)
committerEmil Velikov <emil.l.velikov@gmail.com>
Thu, 16 Feb 2017 15:17:52 +0000 (15:17 +0000)
commit71e00d62ed2228a773a4f5abff98a16961e7f21c
tree9d23916f5f45cc59df33e0adb13986e8ad563c36
parentcb1947eac70f63d78835a5442017b1f3b7099d77
bin/get-extra-pick-list: rework to use already_picked list

Currently we loop (git log --grep) to check if the fix has landed. We
can simplify and make things faster by storing the already_picked list
and grep ping through it.

Slim down the message while we're here.

Cc: "13.0 17.0" <mesa-stable@lists.freedesktop.org>
Signed-off-by: Emil Velikov <emil.velikov@collabora.com>
Reviewed-by: Eric Engestrom <eric.engestrom@imgtec.com>
bin/get-extra-pick-list.sh