More careful identification of @ignore

[Martin Buchholz]

On Thu, Oct 2, 2008 at 11:47, Jonathan Gibbons <Jonathan.Gibbons at sun.com> wrote:
> Egads, 'twould appear t'be true.
>
> As a workaround, I suggest you use the -ignore switch (e.g. -ignore:quiet)
> instead of -k:\!ignore.

I tried -ignore:quiet,
but that appears to have the same bug;
that is, it is not a workaround.

Martin