diff options
Diffstat (limited to 'src/util/git-commit-everything.pl')
| -rwxr-xr-x | src/util/git-commit-everything.pl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/git-commit-everything.pl b/src/util/git-commit-everything.pl index 4d90075..498342a 100755 --- a/src/util/git-commit-everything.pl +++ b/src/util/git-commit-everything.pl @@ -31,8 +31,8 @@ print "Formaline: Committing source tree to git repository...\n"; # Invent a user id if there is none, since newer versions of git # insist on it -system "$git_cmd config user.name || $git_cmd config user.name \"\${USER}\" $silencer"; -system "$git_cmd config user.email || $git_cmd config user.email \"\${USER}\@localhost\" $silencer"; +system "$git_cmd config user.name > /dev/null 2>&1 || $git_cmd config user.name \"\${USER}\" $silencer"; +system "$git_cmd config user.email > /dev/null 2>&1 || $git_cmd config user.email \"\${USER}\@localhost\" $silencer"; # Try to use the previous commit as parent, if possible print "Executing: $git_cmd commit -m $build_id\n" unless $silent; |