diff options
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile index a6f5610938..d1565888eb 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -280,8 +280,8 @@ demos-programs: Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex -Tutorial.v.dvi: ./title.tex Tutorial.v.tex -Tutorial.v.pdf: ./title.tex Tutorial.v.tex +Tutorial.v.dvi: ./version.tex ./title.tex Tutorial.v.tex +Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex # RefMan-ppr.v.tex: ../tactics/eqdecide.cmo |