doc-gen4 find redirects to wrong page

Stream: lean4

[llllvvuu]

(feel free to move this to a better channel if there is one)

This link:

https://teorth.github.io/pfr/docs/find/#doc/ProbabilityTheory.entropy

does find the correct item, but redirects to a slightly wrong URL which gives a 404:

https://teorth.github.io/pfr/docs/PFR/Entropy/Basic.html#ProbabilityTheory.entropy

the correct URL should be:

https://teorth.github.io/pfr/docs/PFR/ForMathlib/Entropy/Basic.html#ProbabilityTheory.entropy

[llllvvuu]

Ah, this was a CI caching issue on our part.

[Notification Bot]

llllvvuu has marked this topic as resolved.

[Notification Bot]

y-samuel has marked this topic as unresolved.