Merge disklog2 into master, attempt 2.

The previous merge went the wrong way (master took precedence over disklog2).
This merge tries to go the correct way:

  git checkout disklog2
  git merge -s ours origin/master
  git checkout master
  git merge disklog2