From 53270e7edb4e16c3ec9cb796aafa3e9e6de89fef Mon Sep 17 00:00:00 2001
From: Greg Wilkins <gregw@intalio.com>
Date: Wed, 12 Jun 2013 13:13:09 +1000
Subject: [PATCH] 410522 JETTY_PORT sets jetty.port property instead of
 -Djetty.port

---
 jetty-distribution/src/main/resources/bin/jetty.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jetty-distribution/src/main/resources/bin/jetty.sh b/jetty-distribution/src/main/resources/bin/jetty.sh
index bfcb1fdabbb..cbd9f24eb44 100755
--- a/jetty-distribution/src/main/resources/bin/jetty.sh
+++ b/jetty-distribution/src/main/resources/bin/jetty.sh
@@ -371,7 +371,7 @@ fi
 #####################################################
 if [ "$JETTY_PORT" ] 
 then
-  JAVA_OPTIONS+=("-Djetty.port=$JETTY_PORT")
+  JETTY_ARGS+=("jetty.port=$JETTY_PORT")
 fi
 
 #####################################################