Skip to content

Commit 3dfd59d

Browse files
committed
update homescreen
1 parent d409c02 commit 3dfd59d

1 file changed

Lines changed: 1 addition & 3 deletions

File tree

vscode/src/vs/workbench/contrib/welcomeGettingStarted/browser/gettingStarted.ts

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -109,9 +109,7 @@ export class GettingStartedPage extends EditorPane {
109109

110110
wrapper.appendChild(document.createElement('h1')).textContent = 'Welcome to Lean4Code';
111111
addParagraph('Welcome to Lean4Code, the customized code editor designed specifically for Lean 4!', 'p', true);
112-
113-
wrapper.appendChild(document.createElement('h2')).textContent = '🚀 Getting started instantly:';
114-
addParagraph('To create a new Lean project, click the ∀ symbol on the top right of this page, or hold down Control + Shift + P (Cmd + Shift + P for Mac OS), to create a new Lean project template');
112+
addParagraph('To create a new Lean project, click the ∀ symbol on the top right of this page, or hold down Control + Shift + P to create a new Lean project template');
115113

116114
wrapper.appendChild(document.createElement('h2')).textContent = '✨ Features';
117115
addParagraph('For any valid lean project, click the robot icon on the left to get started with LeanCopilot, the AI theorem proving assistant!');

0 commit comments

Comments
 (0)