Re: redisplay-dont-pause

[Stefan Monnier]

>> I could if someone wants to work on this, but is it worth doing?
>> If we have no need to support pausing the display any more,
>> it wouldn't be worth spending time to implement this now.
> I agree, so let's wait for the decision by Stefan and Chong whether to
> change the default of this variable.

I don't have any strong opinion on this.  So if you want to change it,
I think it's OK.  Whenever I tried to play with it, it never seemed to
make much difference either way for me.


        Stefan