Substitute all "the the" with "the"

[Tom Tromey]

>>>>> "Дилян" == Дилян Палаузов <dilyan.palauzov@aegee.org> writes:

Дилян> … by applying
Дилян> sed -i "s/the the/the/" `git grep -l "the the"`

I did this and pushed it in.

Tom