Duplication was introduced at merge c78e04645d. Commit
ccc2526 (right-hand side of merge) moved this code from the bottom to
the middle. Commit 21411b4 added a newline at the end of the file,
which made this a conflicted merge; the merge conflict was not resolved
properly.
Fixes#3208.