Re: [Bug-gnubg] Erase player from Player Records fails

[Gary Wong]

On Sat, Jan 11, 2003 at 09:52:08PM +0100, Nardy Pillards wrote:
> It is not possible to erase a Player, if the name of the player has a space
> in it.

Thanks for the bug report.  I've checked in a patch, which should show
up in snapshots dated 030111 and later.

(As a workaround for earlier versions, you can enter the command:

    record erase "player name"

manually, which will work for players whose names contain spaces as long as
you use the quotes.)

Cheers,
Gary.
-- 
   Gary Wong           address@hidden           http://www.cs.arizona.edu/~gary/