-
Notifications
You must be signed in to change notification settings - Fork 46
Open
Labels
enhancementNew feature or requestNew feature or request
Description
For the live.lean-lang.org instance, also due to its nix setup, managing the set of offered projects is somewhat tedious.
It would make it easier if
- the server component would take an environment variable
LEAN4WEB_PROJECT_DIRECTORYto point at the directory that contains all the projects. - there would be no config.tsx file. instead upon server statup, it would enumerate the directories in
LEAN4WEB_PROJECT_DIRECTORY. - a project file could have a
lean4web.jsfile (or similar format) to set- the name shown in the drop-down
- opt-out of being shown there (for projects that we want to host but not advertise)
- other settings like example files.
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request