Close a dangling pull request (#217).

This closes #217.

This pull request already got merged, but for some reason it didn't
close.