minor changes
This commit is contained in:
parent
6a4ed6ec55
commit
e74ba70274
1 changed files with 1 additions and 1 deletions
|
@ -91,7 +91,7 @@ You can fix this error by installing a GNU compatible version of sed, e.g. using
|
|||
brew install gnu-sed --with-default-names
|
||||
```
|
||||
|
||||
## Updating to agda2html
|
||||
## Updating `agda2html`
|
||||
|
||||
Sometimes we have to update agda2html.
|
||||
To update your local copy, run the following commands from your clone of the
|
||||
|
|
Loading…
Reference in a new issue