From 3c9e2699fab4fe6949795de60b876980c360e38d Mon Sep 17 00:00:00 2001
From: Sylvestre Ledru <sylvestre@debian.org>
Date: Sat, 30 Sep 2023 09:00:02 +0200
Subject: [PATCH] build without doc: create an empty directory to please him

---
 debian/rules | 1 +
 1 file changed, 1 insertion(+)

diff --git a/debian/rules b/debian/rules
index 29e5960f..472a5957 100755
--- a/debian/rules
+++ b/debian/rules
@@ -977,6 +977,7 @@ override_dh_prep: build_doc
 
 ifeq ($(DOC_GENERATION), no)
 build_doc:
+	mkdir -p $(CURDIR)/tools/clang/stage2-bins/docs/ocamldoc/html/
 	@echo "Don't build doc on this distro $(DISTRO)"
 else
 build_doc: