extern void print_int_array( int maxw, int nel, int * results, char sep, FILE * out );