diff make-dist @ 107958:09b4b2c3944d

Improve previous change.
author Glenn Morris <rgm@gnu.org>
date Thu, 15 Apr 2010 19:45:26 -0700
parents 1d1d5d9bd884
children 2fb32340c261 43a1fb0eb2d8
line wrap: on
line diff