diff options
author | Uma Zalakain <ping@umazalakain.info> | 2020-05-24 12:15:46 +0100 |
---|---|---|
committer | Bjørn Forsman <bjorn.forsman@gmail.com> | 2020-05-24 14:20:05 +0200 |
commit | 196cc470050dc0764d094df39c0317bb3147dbac (patch) | |
tree | 5f4fbaef950ba31fbe8765606f823705330a0ac8 /doc | |
parent | a036bae1fc517c22232b4b394d3d71b0a2a8bc3f (diff) |
agda: fix typo in library management documentation
Agda expects a "depend" (not "depends") field in the library description.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/languages-frameworks/agda.section.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index 7a5dc767b7c4..8cba6d9faa7d 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -42,7 +42,7 @@ $ agda -l standard-library -i . MyFile.agda ``` name: my-library include: . -depends: standard-library +depend: standard-library ``` - Create the file `~/.agda/defaults` and add any libraries you want to use by default. |