awk 'NR == 1 && $1 != "dbz" {
	print FILENAME, "does not appear to be a dbz file"
	exit 1
}
NR == 1 {
	print "dbz_version", $2
	print "table_size", $3
	print "# (optimized for lines approx. " int($3*0.67) ")"
	printf "separator \\0%o\n", $4
	print "case_rule", $5
	printf "tag_bit 0x%x<<%d\n", $6, $8
	printf "tag_mask 0x%x<<%d\n", $7, $8
	print "bytes", $9
	printf "byte order"
	for (i = 10; i <= NF; i++)
		printf " %d", $i
	printf "\n"
}
NR == 2 {
	print "lines", $1
	printf "lines_history"
	for (i = 2; i <= NF; i++)
		printf " %d", $i
	printf "\n"
}
NR == 3 {
	print "number_untagged", $1
	printf "untagged_history"
	for (i = 2; i <= NF; i++)
		printf " %d", $i
	printf "\n"
}' $1.dir