Compiling helm-lean yields docstring error

Open rommeswi opened this issue 2 years ago • 1 comments

When installing lean-mode from elpa, I get the following error:

In helm-lean-definitions: helm-lean.el:47:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)

This may cause issues while the following is probably minor:

In company-lean--exec: company-lean.el:67:2: Warning: docstring wider than 80 characters

Oct 11 '23 02:10 rommeswi

Lean 3 is EOL

Oct 11 '23 05:10 Kha