From 17ef7376dc998c7e0584411bae55b85b005f753c Mon Sep 17 00:00:00 2001
From: Dmitry Kabanov <dmitry.kabanov@uni-muenster.de>
Date: Mon, 17 Feb 2025 17:35:34 +0100
Subject: [PATCH] [docs] Make sure that `docs/build` dir exists

---
 Makefile | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index f13fb34b..270e3de0 100644
--- a/Makefile
+++ b/Makefile
@@ -35,9 +35,13 @@ clean :
 	$(RM) -r build build.debug build.release
 
 .PHONY : docs
-docs :
+docs : | mk-docs-build-dir
 	cd docs && doxygen && make html
 
 .PHONY : docs-from-scratch
-docs-from-scratch:
+docs-from-scratch: | mk-docs-build-dir
 	cd docs && rm -rf build && doxygen && make html
+
+.PHONY : mk-docs-build-dir
+mk-docs-build-dir:
+	mkdir -p docs/build