diff options
| -rwxr-xr-x | src/util/git-commit-everything.pl | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/util/git-commit-everything.pl b/src/util/git-commit-everything.pl index 5e1d66b..4d90075 100755 --- a/src/util/git-commit-everything.pl +++ b/src/util/git-commit-everything.pl @@ -29,6 +29,11 @@ $ENV{'GIT_DIR'} = "$git_repo/.git"; 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"; + # Try to use the previous commit as parent, if possible print "Executing: $git_cmd commit -m $build_id\n" unless $silent; system "$git_cmd commit -m $build_id $silencer"; |