From 196cc470050dc0764d094df39c0317bb3147dbac Mon Sep 17 00:00:00 2001
From: Uma Zalakain <ping@umazalakain.info>
Date: Sun, 24 May 2020 12:15:46 +0100
Subject: [PATCH] agda: fix typo in library management documentation

Agda expects a "depend" (not "depends") field in the library description.
---
 doc/languages-frameworks/agda.section.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md
index 7a5dc767b7c..8cba6d9faa7 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.