<div dir="ltr"><div class="gmail_extra">What Manuel described is a strict subset of what I asked for. To be honest I don't remember why I asked for that in the first place, as these days I tend to mess around with package lists much less than I did twelve years ago.</div></div>