Reported by Isabel:
HTML editor acts funny (at least on Android Pixel):

• You start writing, you decide to use an intro without puting a . or a space first; the intro is made but the cursor isn't moved (you keep writing where you where) (see video: html editor acts funny with intros.mp4 )
• If you start playing with the eraser and the headings, it seems that the headings are selected even if you changed back to something else (see 40_html editor_headings.jpg )
• UX question (more than anything else): Should the eraser erase ALL kind of format? (Not only work with bold/italics and strikethrough) If it works as it should, maybe we should change order so that the eraser is closed to the ones it can influence..