static char *redo_x16[] = {
	"16 16 7 1",
	" 	c	None",
	"0	c	#000000",
	"1	c	#006600",
	"2	c	#009900",
	"3	c	#00CC00",
	"4	c	#00FF00",
	"5	c	#008000",
	"                ",
	"         1      ",
	"         151    ",
	"        11425   ",
	"     1553344355 ",
	"    5244444435  ",
	"   5344511425   ",
	"   5435  151    ",
	"  5345   1      ",
	"  145           ",
	" 1235           ",
	" 135            ",
	" 525            ",
	" 521            ",
	" 51             ",
	"                "};

static char *redo_x24[] = {
	"24 24 7 1",
	" 	c	None",
	"0	c	#000000",
	"1	c	#006600",
	"2	c	#009900",
	"3	c	#00CC00",
	"4	c	#00FF00",
	"5	c	#008000",
	"                        ",
	"                        ",
	"              1         ",
	"              151       ",
	"              5425      ",
	"            11544351    ",
	"         552234444425   ",
	"       553444444444425  ",
	"      524444444444455   ",
	"     52444421124435     ",
	"     5444351  2455      ",
	"    544425    55        ",
	"    54421     5         ",
	"   53435                ",
	"   1445                 ",
	"  12435                 ",
	"  5345                  ",
	"  5335                  ",
	"  5421                  ",
	"  545                   ",
	"  141                   ",
	"  155                   ",
	"                        ",
	"                        "};

static char *redo_x32[] = {
	"32 32 7 1",
	" 	c	None",
	"0	c	#000000",
	"1	c	#006600",
	"2	c	#009900",
	"3	c	#00CC00",
	"4	c	#00FF00",
	"5	c	#008000",
	"                                ",
	"                                ",
	"                                ",
	"                   1            ",
	"                   151          ",
	"                   2425         ",
	"                   244351       ",
	"                1152444425      ",
	"             552233444444355    ",
	"           553444444444444425   ",
	"          534444444444444435    ",
	"        1244444444444444425     ",
	"       5244444435113444351      ",
	"       544444211  134425        ",
	"      53444451    13351         ",
	"     1244445      155           ",
	"     544445       15            ",
	"     54442                      ",
	"    534435                      ",
	"    14445                       ",
	"    54431                       ",
	"   13441                        ",
	"   53435                        ",
	"   5445                         ",
	"   1445                         ",
	"   5435                         ",
	"   5431                         ",
	"   542                          ",
	"   531                          ",
	"   111                          ",
	"                                ",
	"                                "};

static char **redo_xpm[3] = { redo_x16, redo_x24, redo_x32 };