static void print_element(unsigned int mask, char *element);
/* Values that are bitwise or'd into `toprint'. */
/* Operating system name. */
static void print_element(unsigned int mask, char *element);
/* Values that are bitwise or'd into `toprint'. */
/* Operating system name. */