From 2bcaf3c597292ec2d70b122a1066af1890780c0d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 17 Jun 2024 17:03:23 +0200
Subject: [PATCH] docs: fix typo

---
 docs/dune.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/dune.md b/docs/dune.md
index e45a0a3f..fbceb480 100644
--- a/docs/dune.md
+++ b/docs/dune.md
@@ -16,7 +16,7 @@ Useful links:
 Editor support
 --------------
 
-Good dune support in editors is lacking at the moment, but there are trick you
+Good dune support in editors is lacking at the moment, but there are tricks you
 can play to make it work.
 
 One option is to configure your editor to invoke the `dune coq top` command
-- 
GitLab