From 27dbe3d4ac10c2c913682e83fd90601f0c0a31a9 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 2 Oct 2023 19:44:11 +0200
Subject: [PATCH] Shut up Javadoc errors
---
build.gradle | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/build.gradle b/build.gradle
index 882b232..ecf5634 100644
--- a/build.gradle
+++ b/build.gradle
@@ -71,6 +71,10 @@ compileJava {
dependsOn << 'tom'
}
+javadoc {
+ failOnError = false
+}
+
clean{
delete "src/org/eventb/internal/core/typecheck/TypeUnifier.java"
}
--
GitLab