Le bug porte le numéro 734390 (
https://bugs.launchpad.net/ubuntu/+source/gnome-terminal/+bug/734390). Je voudrais le corriger car le copier-coller marche, j'avais fait une vérification un peu trop rapide. Mais je n'ai pas encore vu comment corriger...