From 901ca2bde5f6bdaa7d7f0809ae7a06cd3f1ee388 Mon Sep 17 00:00:00 2001
From: Ralf Wiebicke <ralf.wiebicke@exedio.com>
Date: Mon, 16 Sep 2024 17:44:58 +0200
Subject: [PATCH] Jenkinsfile#port no longer needed, because docker allows
 reusing ports

---
 Jenkinsfile | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index 8ecd02d8..c1349ad0 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -45,8 +45,8 @@ try
 				    ' "-Dbuild.tag=' + buildTag + '"' +
 				    ' -Dbuild.status=' + (isRelease?'release':'integration') +
 				    ' -Dinstrument.verify=true' +
-				    ' -Dtomcat.port.shutdown=' + port(0) +
-				    ' -Dtomcat.port.http=' + port(1)
+				    ' -Dtomcat.port.shutdown=18005' +
+				    ' -Dtomcat.port.http=18080'
 			}
 
 			recordIssues(
@@ -296,8 +296,3 @@ void assertGitUnchanged()
 		error 'FAILURE because fetching dependencies produces git diff:\n' + gitStatus
 	}
 }
-
-def port(int offset)
-{
-	return 28000 + 10*env.EXECUTOR_NUMBER.toInteger() + offset
-}