On Wednesday, 7 January 2015 at 07:12:33 UTC, Walter Bright wrote:
On 1/6/2015 10:48 PM, Andrei Alexandrescu wrote:
Another one; I tried to use the search box on the top right
corner...
it just resulted in a google search.
Can we do better than that? When people go to the
documentation page,
they want to search the docs, not get a standard google
results page.
That would be quite an involved project. -- Andrei
I find dman.exe to be very handy and use it all the time, but
since it is a hand-built index, it is always hopelessly out of
date.
Why not reuse the index built by chmgen? It's very inclusive and
mostly accurate.
