You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I encountered an issue related to Lean REPL 4.8. (I have some reasons that necessitate the use of this version.)When used as a server, Lean REPL 4.8 requires three '\n' characters to get a response, unlike Lean REPL 4.11, which only needs two. However, using three '\n' characters triggers a formatting issue that causes the server to shut down. Is it possible to modify the internal code of the REPL so that it recognizes two '\n' characters as sufficient for a response?