[kidsil]

F10 always worked for me, but some terminals use F10 for some other functionality.

If that fails, you can click on "10 Quit" with the mouse (not ideal, but an immediate solution).

[protomikron]

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