Upgrade lean to 1.0.177 and I now receive the following error regardless of the lean command I run. E.g.,
lean whoami
Extra data: line 1 column 21977 (char 21976)
Extra data: line 1 column 21977 (char 21976)
<string>:595 Unexpected """ at column 1
Extra data: line 1 column 21977 (char 21976)
Error: <string>:595 Unexpected """ at column 1
Please advise as to which file this error may be coming from and how to fix. As a note, prior versions, down to 1.0.170 also now exhibit the same errors. The issue was not there prior to the upgrade.
Upgrade lean to 1.0.177 and I now receive the following error regardless of the lean command I run. E.g.,
Please advise as to which file this error may be coming from and how to fix. As a note, prior versions, down to 1.0.170 also now exhibit the same errors. The issue was not there prior to the upgrade.