-
Benno Schulenberg authored
When replacements are made, nothing needs to be reset any more (it was done insufficiently anyway). Just make sure the screen is refreshed when all is done -- this may be superfluous when doing interactive replacements, but not when replacing all.
9ec546d2