aboutsummaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
Diffstat (limited to 'man')
-rw-r--r--man/coqdep.12
1 files changed, 1 insertions, 1 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1
index c417402c25..4639a75677 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -106,7 +106,7 @@ Skips subdirectory
Output the given file name ordered by dependencies.
.TP
.B \-boot
-For coq developpers, prints dependencies over coq library files
+For coq developers, prints dependencies over coq library files
(omitted by default).