tree 7c34918c45f02e8543c910c16dbf51d69913727c
parent b73f3d2c7db2e4d9f02ff9d24852685bcb6fa38a
parent 6999c54029b42ea996c2fff4fa37303f79b9d8c2
author Junio C Hamano <gitster@pobox.com> 1306428071 -0700
committer Junio C Hamano <gitster@pobox.com> 1306428071 -0700

Merge branch 'mg/diff-uiconfig-doc' into maint

* mg/diff-uiconfig-doc:
  config.txt,diff-options.txt: porcelain vs. plumbing for color.diff