Hallo Liste, wie kann ich die verschiedenen Profile des gnome2-terminal mit einem Texteditor bearbeiten? Problem: Schriftarten lassen sich nicht richtig einstellen? thx,