char	version[] = "2.12 (5/11/83)";