From 337518f256a3f60ebb19dcf8151a93c674516455 Mon Sep 17 00:00:00 2001 From: Kate Date: Thu, 20 Nov 2025 17:16:33 +0000 Subject: [PATCH] Call man2html only on actual man pages --- doc/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 '