From 96e8e953869dda3629d142cc020660d973fdde2d Mon Sep 17 00:00:00 2001
From: Mattes D <github@xoft.cz>
Date: Mon, 12 Sep 2016 23:23:45 +0200
Subject: CIBuild: Mark as failure on duplicate API docs.

---
 CIbuild.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CIbuild.sh b/CIbuild.sh
index 9e2fa7edb..d652f1d36 100755
--- a/CIbuild.sh
+++ b/CIbuild.sh
@@ -31,4 +31,9 @@ EOF
 		cat ./NewlyUndocumented.lua
 		exit 1
 	fi
+	if [ -f ./DuplicateDocs.txt ]; then
+		echo "ERROR: API documentation has duplicate symbol warnings:"
+		cat ./DuplicateDocs.txt
+		exit 1
+	fi
 fi
-- 
cgit v1.2.3