Search results

<code>npm run production</code> vs <code>npm start</code>

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#59 In leanprover-community/lean4web;

· lecopivo opened on Mar 24, 2025

Potential Bug: Unintended File Access via <code>/api</code> Endpoints

bugSomething isn't workingSomething isn't working

Status: Open.

#58 In leanprover-community/lean4web;

· tautastic opened on Mar 8, 2025

feat: add something like "Error Lens"

enhancementNew feature or requestNew feature or request

future-ideasMaintainers will not work on this but PR welcome!Maintainers will not work on this but PR welcome!

Status: Open.

#51 In leanprover-community/lean4web;

· joneugster opened on Feb 25, 2025

leanOption in lakefile doesn't work

bugSomething isn't workingSomething isn't working

depends-on-external-issue

Status: Open.

#39 In leanprover-community/lean4web;

· timechess opened on Sep 11, 2024

Display notification banners, for example on panic:

enhancementNew feature or requestNew feature or request

Status: Open.

#33 In leanprover-community/lean4web;

· joneugster opened on Aug 11, 2024

Go-to-def

bugSomething isn't workingSomething isn't working

enhancementNew feature or requestNew feature or request

Status: Open.

#31 In leanprover-community/lean4web;

· joneugster opened on Aug 8, 2024

Feature Request: Vim Motions

enhancementNew feature or requestNew feature or request

future-ideasMaintainers will not work on this but PR welcome!Maintainers will not work on this but PR welcome!

Status: Open.

#25 In leanprover-community/lean4web;

· bernborgess opened on May 22, 2024