Si je mets à 9 pt, et que je ré-ouvre, je suis à 0 pt., mais quand j'essaye de changer 12 pt est présélectionné.
Il n'y a pas grand chose dans ce fichier de config, mais:
[gui]
recentrepo = /home/heldwin/test
Il doit y avoir un autre fichier de config, car la taille de la police n'y est pas.
EDIT:
ah si. maintenant j'en ai une, j'avais remis en 9 pt, donc c'est bien le défaut:
[gui]
recentrepo = /home/heldwin/test
fontui = -family \"DejaVu Sans\" -size 10 -weight normal -slant roman -underline 0 -overstrike 0
fontdiff = -family \"DejaVu Sans Mono\" -size 10 -weight normal -slant roman -underline 0 -overstrike 0
EDIT2:
En mettant manuellement à 9, ça passe
EDIT3:
Si je regarde dans le code source, je trouve que ça pour les fonts par defaut:
## config defaults
set cursor_ptr arrow
font create font_ui
if {[lsearch -exact [font names] TkDefaultFont] != -1} {
eval [linsert [font actual TkDefaultFont] 0 font configure font_ui]
eval [linsert [font actual TkFixedFont] 0 font create font_diff]
} else {
font create font_diff -family Courier -size 10
catch {
label .dummy
eval font configure font_ui [font actual [.dummy cget -font]]
destroy .dummy
}
}
Mais s'il ne trouve rien, il devrait mettre en Courier 10, pas DejaVu 9
Ou alors ça passe dans le catch et ça ferait: eval font configure font_ui [font actual [.dummy cget -font]]
(car je ne trouve pas de font "Courier", que un "Courier 10 Pitch")