[plt-scheme] how to reset help-desk's search cache?

On Sun, Mar 05, 2006 at 04:38:32PM -0600, Robby Findler wrote:
> There is, but only if you are using an SVN-built installation. Go to
> the manuals page (from the first page of Help Desk (click the "Home"
> button on the top of Help Desk to get back there)) and follow the
> "flush index and keywords cache".

Oh!  *That's* what that does!  Perfect.

> planet, after installing something, should be (either directly or
> indirectly) triggering this refresh. I'm not sure how to accomplish
> that tho, since that would mean that a program running inside DrScheme
> could tickle DrScheme's state. One of the many many things that planet
> tickles! sigh.

Indeed.

If it helps, I generally do the planet installation either by using the
command-line tool or by firing up MzScheme and typing in the (require
(planet ...)) form there, not by using the running DrScheme.

Thanks,

Richard