fix: initial commit not working on fresh Git install

leanprover · Jul 26, 2024 · f614055 · f614055
1 parent 0bab1db
commit f614055
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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 },
         )