Comment by protomikron

Ah I see, thx, it's a pretty default configured "gnome-terminal", which probably captures the F10.