doc-gen not showing sum notation

Stream: general

[Eric Wieser]

Compare

https://cs.brown.edu/courses/cs1951x/docs/find/finset.sum_filter

With

docs#finset.sum_filter

Did this get broken at the doc-gen end or by lean?

[Eric Wieser]

Somehow it seems this line isn't running:

https://github.com/leanprover-community/doc-gen/blob/6e2b968f421b14a4d7b4a9c14dd84aa47a9b58a6/src/entrypoint.lean#L4

[Eric Wieser]

Maybe it needs to be called from within main otherwise it acts on a temporary environment?