Issue with installation

[rshlyakh]

When installing LeanCopilot, I got an error on line 36 of LeanCopilot/Frontend.lean, which caused the build to fail.

Changing the line from:
| some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).takeWhile (· != '\n'))

To:

| some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).takeWhile (· != '\n')).toString

Seems to resolve the issue.

[Peiyang-Song]

Indeed, that was likely due to a recent update in dependency packages. Fixed now. Thank you very much for sharing the note!