What happened to the search functionality in #tpil and #fpil

Stream: general

[Ching-Tsun Chou]

It seems that the search functionality in both #tpil and #fpil are gone. (Fortunately, it is still in #mil.). Will they be restored? Lack of search capability makes these documents far less usable. Now I have to do "git grep" in their git repo to find anything.

[Ching-Tsun Chou]

BTW, "#fpil" points to an older document: https://leanprover.github.io/functional_programming_in_lean/. What I meant is https://lean-lang.org/functional_programming_in_lean/