<?php
  include 'misc.inc.php';

  print "<?php\n\n";
  print "   function print_page_header() {\nprint <<<END\n";
  print_page_header();
  print "\nEND;\n}\n\n";

  print "   function print_page_footer() {\nprint <<<END\n";
  print_page_footer();
  print "\nEND;\n}\n\n";
  print "?>\n\n";
?>