[PATCH] Fix PR cli/15603

[Jan Kratochvil]

On Tue, 18 Jun 2013 16:28:13 +0200, Tom Tromey wrote:
> Here's a new version that I think addresses your comments.
> 
> Let me know what you think.

Yes, I am fine with this patch.


Thanks,
Jan