diff options
| author |  Martin Vassor <martin.vassor@epfl.ch> | 2017-12-11 18:04:57 +0100 |
|---|---|---|
| committer | Martin Vassor <martin.vassor@epfl.ch> | 2017-12-11 18:04:57 +0100 |
| commit | 1f8bb04a428bb76d05b7d277ad91a6a2acefe63c (patch) | |
| tree | a1fbae742b4961188b88458175abb61162415ebb /tools/CoqMakefile.in | |
| parent | 0275b5802ffd416dd0ed739955445a1c3c0287e9 (diff) | |
Fix issue #6387
Diffstat (limited to 'tools/CoqMakefile.in')
| -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 |