Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Jan 13, 2025
1 parent a106c1f commit 8eb0ec7
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,12 @@ The website parses arguments of the form `https://myserver.com/#arg1=value1&arg2
The recognised arguments are:

- `code=`: plain text code.
(overwrites `codez`)
*(overwrites `codez`; note this argument does accept unescaped code, but the browser will always display certain characters escaped, like `%20` for a space)*
- `codez=`: compressed code using [LZ-string](https://www.npmjs.com/package/lz-string).
- `url=`: a URL where the content is loaded from.
(overwrites `code` and `codez`).
- `project=`: the Lean project used by the server to evaluate the code. This has the be the name
of one of the projects the server defines in their config.
*(overwrites `code` and `codez`)*.
- `project=`: the Lean project used by the server to evaluate the code. This has to be the name
of one of the projects defined in the server's config.

The server will automatically only write one of `code`, `codez`, and `url` based on the following
logic:
Expand Down

0 comments on commit 8eb0ec7

Please sign in to comment.