From f6140552b779562cd43e70169d81b13e3a785f5f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 26 Jul 2024 09:34:24 +0200 Subject: [PATCH] fix: initial commit not working on fresh Git install --- 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..fd160d420 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 }, )