Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Dec 18, 2023
1 parent 19a307d commit a33976a
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Projects/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ To add a new project, one needs to add a lean project here.
Projects can be any Lean projects.

1. You can build the lean project manually. For automatic updates, your project should include a file `ProjectName/build.sh` which can be
executed to build the project. See `lean4web-tools` for an example.
executed to build the project. See [lean4web-tools](https://github.com/hhu-adam/lean4web-tools) for an example.
2. Your project should add the dependency
```lean
require webeditor from git
"https://github.com/hhu-adam/lean4web-tools.git" @ "main"
```
in its `lakefile.lean`. This package adds some simple tools like `#package_version`.
4. For a project to appear in the settings, you need to modify `Settings.tsx` and add a new option with value `ProjectName`.
3. For a project to appear in the settings, you need to modify `Settings.tsx` and add a new option with value `ProjectName`.

0 comments on commit a33976a

Please sign in to comment.