diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 00:00:29 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-14 00:00:29 +0100 |
| commit | e32f176cf8f8637aee98c5335af7e4b3e375aed3 (patch) | |
| tree | bd918258241200c2c36087dd07f7f71ad66cdd69 /tools | |
| parent | 671c4dbd064884a042d8f2bea5186ab5c7eaaeec (diff) | |
| parent | 1f8bb04a428bb76d05b7d277ad91a6a2acefe63c (diff) | |
Merge PR #6388: Fix issue #6387
Diffstat (limited to 'tools')
| -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 6e87e67bb..80b1f584b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -434,7 +434,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 |