> We're wondering here whether we should push out 5.04.2 soon, or wait a > while and see what other bugs turn up. > > Opinions, anyone? Release often, release soon! Why not put out a source distribution on a regular basis, say, every month or so (I realize that binary distributions are a lot of work). Cheers, Ralf