Revert "Close #772."

This reverts commit 859c5db1f089f7ece73a3706e94b7ef4262cf72b.