Separate git branch for documentation

[Carl D. Sorensen]

Some time in the past, there was a request for a separate git
repository/branch[1] for documentation, with the idea that more people could
be approved for push access on the docs repository/branch than would be
approved for push access on the code.

I think it would also be easier to have a separate branch for the docs
because it would facilitate debugging -- there are lots more docs commits
than code commits, so it's hard (for me at least) to do a good job of
bisecting when I'm looking for code changes.  If we can come up with some
method for isolating doc changes from code changes, I think it would be
helpful.

Thanks,

Carl

1.  I'm not sure what the correct term here is.  I just want to be able to
separate docs commits from code commits.