#define NULL (char *) 0
int reportbugs_text_length = 3;
char *reportbugs_text[] = { 
  "reportbugs.text",
  "",
  "Maintained by Lorenzo Bettini <http://www.lorenzobettini.it>",
  "Report bugs to <bug-source-highlight at gnu.org>",
  NULL };