WidthValue        204 src/androidgui.h #define WidthValue  	0x0004
WidthValue         78 src/haikugui.h #define WidthValue  	0x0004
WidthValue        125 src/nsgui.h    #define WidthValue  	0x0004
WidthValue         80 src/pgtkgui.h  #define WidthValue  	0x0004
WidthValue         72 src/w32gui.h   #define WidthValue  	0x0004