On Tue, 26 Feb 2019 02:39:14 +0100, Ingo Schwarze wrote:

> In that case, let's just use an index rather than a pointer;
> diff otherwise unchanged.

OK millert@

 - todd

Reply via email to