We build those PDF files when we create release tarfiles.  (I believe "make 
pdf" in the build directory corresponding to src/doc will create them.)  I 
guess we could add some text to README discussing the differences between a 
git checkout and a release, since it's not uncommon for people to consume 
our source tree in that way.