Apply suggestions from code review

3 years ago · 96a8da9d93
parent e947c434a8
commit 96a8da9d93
1 changed files with 1 additions and 1 deletions
--- a/server/adam/Adam.lean
+++ b/server/adam/Adam.lean
@ -27,7 +27,7 @@ Introduction

 Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte
 Beweisführung. Das Interface ist etwas vereinfacht, aber wenn du den *Editor Mode* aktivierst, fühlt es sich 
-fast genauso an wie eine professionalle IDE, etwa VSCode.
+fast genauso an wie in VSCode, der standard IDE für Lean.

 Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels,
 die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.