With Peter's latest commit, there aren't any actual scripts left in
src/bin/scripts; only C programs. Does that bother anyone? I was
wondering about renaming to something like src/bin/misc. (Not that
that name seems very compelling either...)
regards, tom lane