Skip to content
This repository has been archived by the owner on Aug 5, 2024. It is now read-only.

Compiling helm-lean yields docstring error #47

Open
rommeswi opened this issue Oct 11, 2023 · 1 comment
Open

Compiling helm-lean yields docstring error #47

rommeswi opened this issue Oct 11, 2023 · 1 comment

Comments

@rommeswi
Copy link

rommeswi commented Oct 11, 2023 •
edited
Loading

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
@Kha
Copy link
Member

Kha commented Oct 11, 2023

Lean 3 is EOL

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Kha @rommeswi