remove leanagent content

Author: wadkisson

vscode/extensions/leanagent-panel/package.json

@@ -84,7 +84,7 @@ gettingStartedContentRegistry.registerProvider('lean4code_welcome', () => `
 	<p style="margin-bottom: 0.25rem; font-size: 0.9rem;">To trace any lean project using LeanDojo, simply click the dojo icon on the left hand panel. Enter a name for the trace, and the url and the most recent commit hash (you can find it on GitHub by clicking the circular clock icon right under the green "code" button for any repo, and then clicking the copy button for any commit) of the repo you want to trace. Then, add in your GitHub personal access token. Finally, paste in the version of Lean the repo to trace is using (i.e., paste in the contents of the repo's "lean-toolchain" file. From there, follow the instructions on the left hand side, and wait for your trace to complete!</p>
 	<p style="margin-bottom: 0.25rem; font-size: 0.85rem;">-New to LeanDojo? Read up on it here: <a href="https://leandojo.org/" style="color: #4FC3F7; text-decoration: underline;" target="_blank">https://leandojo.org/</a></p>
 
-	<p style="margin-bottom: 0.25rem; font-size: 0.85rem;">We're still working on more tools for Lean4Code, including more integrated LeanDojo features, and a implementation of LeanAgent.</p>
+	<p style="margin-bottom: 0.25rem; font-size: 0.85rem;">We're still working on more tools for Lean4Code, including more integrated LeanDojo features.</p>
 
 	<div style="border: 1px solid #666; padding: 0.75rem; margin: 1rem 0; border-radius: 4px; background-color: rgba(255, 255, 255, 0.05);">
 		<p style="margin: 0; font-size: 0.8rem;">This is the beta version of Lean4Code. This is our first iteration of the app, and is not meant to be a final product. Please report any errors you encounter using Lean4Code using the issues tab, or send an email to <a href="mailto:adkisson@wustl.edu" style="color: #4FC3F7; text-decoration: underline;">adkisson@wustl.edu</a></p>