On Mon, 2002-07-22 at 13:45, Jesper Skov wrote: > > David, if you maintain some docs for how to tweak the preferences, you > may want to mention the color settings there. >
I don't, but it would be a good idea. Which options do you tweak for this, and how? Thanks, David -- David Chart
