fix: dummy git identity in test to make runner happy

leanprover · Jun 30, 2022 · 1501702 · 1501702
1 parent a34343d
commit 1501702
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/test/84/test.sh b/test/84/test.sh
@@ -8,6 +8,8 @@ LAKE=${LAKE:-../../build/bin/lake}
 $LAKE new a
 pushd a
 git add .
+git config user.name test
+git config user.email [email protected]
 git commit -am 'first commit in a'
 popd
 
@@ -18,6 +20,8 @@ require a from git "../a" @ "master"
 EOF
 ../$LAKE update
 git add .
+git config user.name test
+git config user.email [email protected]
 git commit -am 'first commit in b'
 popd