font e font [file] - forse glossario

[Francesco Potorti`]

>> Per inciso, per me tradurre "font" in "caratteri" come nella quotatura di
>> sopra è sbagliato. I caratteri sono una cosa, i font un'altra. Semmai
>> "tipo di caratteri" (che mi pare stia pure nel glossario), ma è
>> inutilmente lungo e pesante.
>Il problema della lunghezza, peraltro, e` particolarmente sentito nel caso
>di applicazioni grafiche. Ad esempio, in gnome-control-center, tradurre
>"font" con "tipo di carattere" comporterebbe notevoli problemi di
>dimensionamento delle finestre.

Per favore, un grano di sale.

I "font" sono i "tipi di carattere".

Ma se vedo scritto "cannot use Times font" traduco
 "impossibile usare il carattere Times".

Il "tipo di" è necessario quando si deve chiarire la carattreristica
del carattere di cui si parla, ma se si sta già indicando il nome di un
tipo di carattere, diventa inutile.