From f57d8e159512331c0dc73c934683d6ca10c95444 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 28 Oct 2024 17:47:17 +0100
Subject: [PATCH] Remove unused Gradle eclipse plugin

---
 tlatools/org.lamport.tlatools/build.gradle | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tlatools/org.lamport.tlatools/build.gradle b/tlatools/org.lamport.tlatools/build.gradle
index 0e34dfea6..230796d94 100644
--- a/tlatools/org.lamport.tlatools/build.gradle
+++ b/tlatools/org.lamport.tlatools/build.gradle
@@ -1,5 +1,4 @@
 apply plugin: 'java'
-apply plugin: 'eclipse'
 apply plugin: "maven-publish"
 apply plugin: "signing"
 
-- 
GitLab