aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tools/CoqMakefile.in2
1 files changed, 1 insertions, 1 deletions
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