Re: typo in couple of places

On Mon, 9 Oct 2023 at 16:17, Amit Kapila <amit(dot)kapila16(at)gmail(dot)com> wrote:
>
> On Sat, Oct 7, 2023 at 8:28 AM vignesh C <vignesh21(at)gmail(dot)com> wrote:
> >
> > On Fri, 6 Oct 2023 at 20:50, Dagfinn Ilmari Mannsåker <ilmari(at)ilmari(dot)org> wrote:
> > >
> > > vignesh C <vignesh21(at)gmail(dot)com> writes:
> > >
> > > > Hi,
> > > >
> > > > I noticed a couple of typos in code. "the the" should have been "the",
> > > > attached patch has the changes for the same.
> > >
> > > This made me curious about other duplicate word occurrences, and after a
> > > few minutes of increasingly-elaborate regexing to exclude false
> > > postives, I found a few more (plus a bonus a _missing_ "the"). See the
> > > attached patch (which includes your originl one, for completeness).
> >
> > Thanks, Looks good.
> >
>
> Pushed.

Thanks for pushing this.