diff options
author | 2017-12-11 18:04:57 +0100 | |
---|---|---|
committer | 2017-12-11 18:04:57 +0100 | |
commit | 1f8bb04a428bb76d05b7d277ad91a6a2acefe63c (patch) | |
tree | a1fbae742b4961188b88458175abb61162415ebb | |
parent | 0275b5802ffd416dd0ed739955445a1c3c0287e9 (diff) |
Fix issue #6387
-rw-r--r-- | tools/CoqMakefile.in | 2 |
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 |