This depends on issue #528. `make install` should do the right thing.
This depends on issue #528.
make installshould do the right thing.