From 9b412a1f3dfb10a967a31c01cb65db0292d7db6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jun 2019 13:55:51 -0700 Subject: [PATCH] configure git identity Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.cmd | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/mk_win_dist.cmd b/scripts/mk_win_dist.cmd index 66b9747ed..bbe7de5ae 100644 --- a/scripts/mk_win_dist.cmd +++ b/scripts/mk_win_dist.cmd @@ -1,3 +1,7 @@ +git config --global user.email "nbjorner@microsoft.com" + +git config --global user.name "Nikolaj Bjorner" + call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" python scripts\mk_win_dist.py --x64-only --dotnet-key=$(Agent.TempDirectory)\z3.snk