diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts index d109a65b..3421fab9 100644 --- a/vscode-lean4/src/projectinit.ts +++ b/vscode-lean4/src/projectinit.ts @@ -392,7 +392,7 @@ Open this project instead?` const result: ExecutionResult = await batchExecuteWithProgress( 'git', - ['clone', projectUri, projectFolder.fsPath], + ['clone', '--depth=1', projectUri, projectFolder.fsPath], downloadProjectContext, 'Cloning project', { channel: this.channel, allowCancellation: true },