Hi, наб <nabijaczlew...@nabijaczleweli.xyz> wrote: > Hi! > > On Wed, Oct 14, 2020 at 12:12:14AM +0200, Holger Wansing wrote: > > I have pushed this now. > > Let's see how it goes. > > It's been a few days, enough, I'd think, for the change to have > propagated; however both grub-pc and a fresh package, such as > https://packages.debian.org/sid/gnuradio > which is at version 3.8.2.0-4 (Thu, 15 Oct 2020 00:20:23 -0400), > uploaded on Mon, 19 Oct 2020 03:04:05 +0000: > https://tracker.debian.org/news/1184204 > has the Tags: link pointing at > https://debtags.alioth.debian.org/edit.html?pkg=gnuradio
Yes, you are right. As it seems, a manual action on picconi.debian.org is required to get the changes propagated to the webpage: a 'git pull' seems to be required there in /srv/packages.debian.org/ However, I noticed just this monday morning that I cannot get the needed permissions to do this, so maybe someone from the webmaster team can do this? Thanks Holger -- Holger Wansing <hwans...@mailbox.org> PGP-Fingerprint: 496A C6E8 1442 4B34 8508 3529 59F1 87CA 156E B076