static const char *colorname[NUMCOLS] = { "black", /* after initialization */ "#005577", /* during input */ "#CC3333", /* failed/cleared the input */ }; static const Bool failonclear = True;