BEGIN {
	printf("%.1a\n", 42)
}