From c9bb0e87c91beae3e17a829603e4459cf804ec51 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= <git@maximilian-kessler.de>
Date: Mon, 31 Jan 2022 00:46:15 +0100
Subject: [PATCH] tolerate documentation folder in build directory

---
 build/build.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build/build.py b/build/build.py
index 216cd15..c137f34 100644
--- a/build/build.py
+++ b/build/build.py
@@ -148,7 +148,7 @@ def build(
                     file.unlink()
             elif not str(file.relative_to(output_dir)) in built_files:
                 if not file.is_dir() and not str(file.relative_to(output_dir)) == 'build_info.json':
-                    if '.git' not in str(file):
+                    if '.git' not in str(file) and 'documentation/' not in str(file):
                         # PyTeX does not at all know something about this file
                         raise UnknownFileInBuildDirectoryError(file.relative_to(output_dir))