Fix up doc building

Unbreak build after 988cd77462865f25d76db1684df183125565e359 shuffled
file names around without changing the corresponding Makefile.