#!/usr/bin/awk -f
BEGIN {
print "// generated file, do not edit by hand"
}
{
printf "char str_%s[] = \"%s\" ;\t\t// %d\n", $2, $2, $1
END {