| 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? Robby
| Posted on the users mailing list. |
|
![[logo]](/logo.png){kind=logo}