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.
mantisbt · Sep 20, 2017 · e8b45c2 · e8b45c2
1 parent 722540a
commit e8b45c2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docbook-manual-repo.py b/docbook-manual-repo.py
@@ -66,7 +66,7 @@ def git_current_branch():
 
 
 def git_checkout(branch):
-    os.system('git checkout -f %s' % branch)
+    os.system('git checkout -f %s >/dev/null' % branch)
 
 
 def main():