From: Jakub Jirutka <jakub@jirutka.cz>
Date: Thu, 28 Oct 2021 01:27:53 +0200
Subject: [PATCH] Disable HTML docs, install only man pages

HTML docs are big and they are available only anyway.

--- a/doc/src/sgml/Makefile
+++ b/doc/src/sgml/Makefile
@@ -16,7 +16,7 @@
 # to want to use.
 html:
 # Note that all is *not* the default target in this directory
-all: html man
+all: man
 
 # We don't need the tree-wide headers or install support here.
 NO_GENERATED_HEADERS=yes
@@ -202,14 +202,14 @@
 ## Install
 ##
 
-install: install-html install-man
+install: install-man
 
 installdirs:
-	$(MKDIR_P) '$(DESTDIR)$(htmldir)'/html $(addprefix '$(DESTDIR)$(mandir)'/man, 1 3 $(sqlmansectnum))
+	$(MKDIR_P) $(addprefix '$(DESTDIR)$(mandir)'/man, 1 3 $(sqlmansectnum))
 
 # If the install used a man directory shared with other applications, this will remove all files.
 uninstall:
-	rm -f '$(DESTDIR)$(htmldir)/html/'* $(addprefix  '$(DESTDIR)$(mandir)'/man, 1/* 3/* $(sqlmansectnum)/*)
+	rm -f $(addprefix  '$(DESTDIR)$(mandir)'/man, 1/* 3/* $(sqlmansectnum)/*)
 
 
 ## Install html