HTML editor on Linux question