This reverts commit 554347e0. For some weird reason, this fixed the `make check` but broke the `make distcheck`. I am lost. Better revert, and now distcheck works great.