#!/usr/bin/awk -f

BEGIN\
{
    print "// Do not edit this file (edit \""ARGV[1]"\", and run \"make\").\n"
    if (ARGC > 2) { print ARGV[2]; ARGC = 2 }
}

{
    gsub("\\\\", "\\\\");
    gsub("\\\"", "\\\"");
    print "\""$0"\\n\""
}