diff make-dist @ 80793:7aad137aaf4e

Copy in some minor bug fixes from the trunk.
author Alan Mackenzie <acm@muc.de>
date Wed, 03 Sep 2008 21:01:12 +0000
parents 5e73f3fa746f
children f13d2ef47961
line wrap: on
line diff