bug#4922: <control>

[Drew Adams]

> >> > And AFAICT it does seem to be fixed.  Should it be closed?
> >> >
> >> > http://debbugs.gnu.org/cgi/bugreport.cgi?bug=16216
> >>
> >> That 16216 is a duplicate of this bug, isn't it? Since it is fixed the
> >> original is also fixed.
> >
> > Yes, except it is the other way around.  AFAICT, that bug (and
> > so this one) has already been fixed.
> >
> > But perhaps Fuqiao is seeing something different and there is
> > still a bug somewhere.
>
> As the original reporter from 2011 I maintain that that is the
> original, and not the one from last December. What I meant with "since
> it is fixed the original is also fixed" was that it was the copy that
> finally triggered the fix.

I see what you are saying.  AFAICT:

1. Yes, 16216 is a duplicate of 4922 (I had it backward; sorry).

2. Yes, it was the duplicate, 16216 that triggered fixing (by Eli).

3. Yes, it seems to be fixed.

4. But we should perhaps wait to hear from Fuqiao wrt whether
he can repro it with the latest code.

If he can confirm that this is fixed, 4922 and 16216 can be
closed (no?).