Skip to content

Commit

Permalink
[ doc ] missing test blurb
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais committed Oct 27, 2023
1 parent 440cee2 commit 4425548
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions www/source/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,12 @@ you will need to pass `-p linear` to `idris2` to use modules defined in it.
Similarly to `contrib` and `linear`, you will need to pass `-p network`
to `idris2` to use modules defined in it.

#### [Test](https://idris-lang.github.io/Idris2/test)

`test` is the add-on to `base` you'll need to write test suites.
Similarly to other add-ons, you will need to pass `-p test` to
`idris2` to use modules defined in it.

#### [Papers](https://idris-lang.github.io/Idris2/papers)

`papers` is not installed by default.
Expand Down

0 comments on commit 4425548

Please sign in to comment.