[racket] ranking of search results in documentation search

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Mon Jun 4 21:51:50 EDT 2012

On Mon, Jun 4, 2012 at 8:31 PM, Eli Barzilay <eli at barzilay.org> wrote:
> 6 hours ago, Greg Hendershott wrote:
>> > This would be easy to play with: click the [!] and you get a
>> > dialog with preferences.
>> Ah, I'd never noticed the [!].
> Random thought: now that a gear icon is conventional for settings,
> would it help if it changes to "[*]"?

I couldn't resist replying here: why not an actual gear icon?


Posted on the users mailing list.