aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-01-06 17:57:44 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-01-06 17:57:55 +0100
commitbf16900f43c1291136673e7614587fe51eebc88f (patch)
treeedc8a80c3c2145aa6a68c9cad63c6f42ef0d6d47 /Makefile.common
parent2b00f74f104586c8d8b205161320e850efa91268 (diff)
Fix some documentation typos.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index fead1dac6..7c98b64de 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -78,12 +78,12 @@ SRCDIRS:=\
IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
-# Order is relevent here because kernel and checker contain files
+# Order is relevant here because kernel and checker contain files
# with the same name
CHKSRCDIRS:= checker lib config kernel parsing
###########################################################################
-# tools
+# Tools
###########################################################################
COQDEP:=bin/coqdep$(EXE)