From e15359532db1a80a6915459dc619db46330c02db Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 26 Jul 2024 12:00:37 +0200 Subject: [PATCH] fix: initial commit not working on fresh Git install (#512) --- vscode-lean4/src/projectinit.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index f2bac1f78..d62d9502f 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -191,9 +191,12 @@ export class ProjectInitializationProvider implements Disposable { return 'GitAddFailed' } + const author = 'Lean 4 VS Code Extension' + const email = '<>' + const gitCommitResult = await batchExecute( 'git', - ['commit', '--author', 'Lean 4 VS Code Extension <>', '-m', 'Initial commit'], + ['-c', `user.name='${author}'`, '-c', `user.email='${email}'`, 'commit', '-m', 'Initial commit'], projectFolder.fsPath, { combined: this.channel }, )