Tools: master e8b45c28

Diff Back to Repository
Author Committer Branch Timestamp Parent
dregad dregad master 2017-09-19 02:52 master 722540a8
Changeset

Redirect git checkout output to /dev/null

This avoids cluttering the log file - when redirecting STDOUT, git
checkout still displays information about the previous and new HEAD.
mod - docbook-manual-repo.py Diff File