Include a file from a git tag

This change allows inclusion of code from a specific git tagged version
of a file.  It looks for the given tag/filename in the local git repo;
it is not currently possible to specify a different repo.

The file is checked out into a temporary directory and included into the
book, and then the temp directory is deleted.  The operation thus has
no effect on the state of the repository.