[Tustep-Liste] EDITOR: Textfarbe aendern

[pstahl at cc.jyu.fi]

Michael Trauths Hinweis, dass das
> eine *sehr* nuetzliche Funktion [sei], die noch viel zu
> wenig bekannt ist und in der Folge natuerlich auch viel zu
> wenig benutzt wird
könnte doch auch Anlass sein, diese Farbeinstellung in die
Voreinstellungen des Editors aufzunehmen. Ich weiß, dass
die Entwicklergruppe in Tübingen sehr zurückhaltend mit
allen derartigen Einstellungen ist. Aber vielleicht
kann Herr Schälkle dazu bitte kurz Stellung nehmen.

Beste Grüße
P.Stahl