#! /usr/bin/gawk -f
# Last edited on 1999-01-02 07:36:30 by stolfi

# Removes the headers and intial/final empty "#" lines


BEGIN {
  initial = 1;
}

/^# *[Dd]escription[:]? *$/ { next; }

/^# *[Cc]omment[s]?[:]? *$/ { next; }

/^ *$/ { next; }

/^# *$/ { if (! initial) { blank++; }; next; }

/^#/ { while (blank > 0) { print "#"; blank--; }; print; initial = 0;  next; }

// { print "bad format" > "/dev/stderr"; }