From 635c9c4b1f99247cacbb01bb5b3727abda2d11b4 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 28 Oct 2024 17:33:32 +0100
Subject: [PATCH] Add comment about why javadoc.failOnError is disabled
---
tlatools/org.lamport.tlatools/build.gradle | 2 ++
1 file changed, 2 insertions(+)
diff --git a/tlatools/org.lamport.tlatools/build.gradle b/tlatools/org.lamport.tlatools/build.gradle
index 5d0760174..c304e28fc 100644
--- a/tlatools/org.lamport.tlatools/build.gradle
+++ b/tlatools/org.lamport.tlatools/build.gradle
@@ -33,6 +33,8 @@ java {
}
javadoc {
+ // The TLA Tools source code uses unescaped HTML symbols in Javadoc text,
+ // which is considered an error.
failOnError = false
}
--
GitLab