diff --git a/doc/Makefile b/doc/Makefile index 011d66d1454..e94b4c38072 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -38,7 +38,7 @@ man-html: echo '' >>$@/index.html echo '

Opam $(version) man-pages index

' >>$@/index.html echo '