Con el rollo de los bugs y demás, he terminado por "limpiar" mi usuario por el procedimiento de
a) Entrar con otro usuario y cambiar el nombre de la carpeta /home/jorge (que es mi home, claro)
b)Crear otra carpeta /home/jorge y darle como propietario al usuario jorge
c)Volver a entrar con ese usuario al sistema y
d)Mover los archivos de Datos del viejo usuario al nuevo.
Todo perfecto y los problemas desaparecen peeeero
La fuente por defecto de los programas de gambas, que antes era ubuntu 10, ahora es DejaVu Sans 12, lo que hace que los programas sean como muy aparatosos.
Nada que ver con las fuentes que tiene el Cinnamon.
¿Alguien sabe de dónde sale ese DejaVu ?