log make-dist @ 112453:06719a229a46 default tip

age author description
Fri, 14 Jan 2011 13:12:57 -0800 Paul Eggert Merge from mainline.
Fri, 14 Jan 2011 10:14:17 -0800 Paul Eggert Merge from mainline.
Sat, 08 Jan 2011 23:29:26 -0800 Paul Eggert Use gnulib's getopt-gnu module.