RE: Should we kill off the headers in Tools>Preferences?

[Leuven, E.]

> I wonder if there would be objections....

there always are.

but in this case not too many i would think.

so i suggest we put it in while the others are not watching...