> On 30-Oct-2022, at 5:18 PM, Nils Breunese <[email protected]> wrote: > > Oops, I even obsoleted that port myself. Ok, ignore openjdk7-zulu as an > example, but my point still stands for other removed ports.
(Sending again because previous one seems to have been rejected due to wrong ‘from’ email) Yeah, these few ports fell into the edge-case of how we handle incremental git updates, particularly due to the directory change to java/openjdk-distributions/Portfile . To handle such cases there is a weekly job that does a full refresh, but it wasn’t running for some reason. I have triggered the job and it seems to have fixed this (the openjdk page now show shows it as deleted), the search index will also get fixed in a day or two. Thanks for sharing this, please check if you are still seeing this mismatch for any other ports.
