From 3e0bf68bdc1ac6bde7bd04236657fb4d554817ad Mon Sep 17 00:00:00 2001
From: mcaci
Date: Sat, 12 Oct 2019 14:24:18 +0200
Subject: Doc update with mlg extension - fix #10855

---
 tools/CoqMakefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index d37d2bea94..08253e5a8f 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -266,7 +266,7 @@ CMIFILES = \
 	$(CMOFILES:.cmo=.cmi) \
 	$(MLIFILES:.mli=.cmi)
 # the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
-# a .ml4 file
+# a .mlg file
 CMXSFILES = \
 	$(MLPACKFILES:.mlpack=.cmxs) \
 	$(CMXAFILES:.cmxa=.cmxs) \
-- 
cgit v1.2.3