Unicode alternative for '..' (ticket #3894)

[Yitzchak Gale]

I wrote:
>> My opinion is that we should either use TWO DOT LEADER,
>> or just leave it as it is now, two FULL STOP characters.

Simon Marlow wrote:
> Just to be clear, you're suggesting *removing* the Unicode alternative for
> '..' from GHC's UnicodeSyntax extension?

Yes, sorry. Either use TWO DOT LEADER, or remove
this Unicode alternative altogether
(i.e. leave it the way it is *without* the UnicodeSyntax extension).

I'm happy with either of those. I just don't like moving the dots
up to the middle, or changing the number of dots.

Thanks,
Yitz