From 1f8bb04a428bb76d05b7d277ad91a6a2acefe63c Mon Sep 17 00:00:00 2001
From: Martin Vassor <martin.vassor@epfl.ch>
Date: Mon, 11 Dec 2017 18:04:57 +0100
Subject: Fix issue #6387

---
 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 7fd942908..948f15d09 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -432,7 +432,7 @@ all.pdf: $(VFILES)
 		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
 
 # FIXME: not quite right, since the output name is different
-gallinahtml: GAL=g
+gallinahtml: GAL=-g
 gallinahtml: html
 
 all-gal.ps: GAL=-g
-- 
cgit v1.2.3