agda: fix typo in library management documentation

Agda expects a "depend" (not "depends") field in the library description.
2020-05-24 14:20:05 +02:00
parent a036bae1fc
commit 196cc47005
1 changed files with 1 additions and 1 deletions
@@ -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.