Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Mar 14, 2024
1 parent 656303d commit e936b12
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,11 @@ you will need to modify the following files:
## Development Instructions

Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repository, run:
1. `npm install` to install dependencies
2. run `npm run build_server` to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project)
3. and then `npm start` to start the server

1. `npm install`, to install dependencies
2. `npm run build_server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project)
3. `npm start`, to start the server.

The project can be accessed via http://localhost:3000. (Internally, websocket requests to `ws://localhost:3000/`websockets will be forwarded to a Lean server running on port 8080.)

## Running different projects
Expand Down

0 comments on commit e936b12

Please sign in to comment.