423397 - Jetty server does not run on Linux server startup because of

a bug in jetty.sh script.

Fixed by using the "*" instead of "+" for numbers so that sed does not
complain and it's also non-GNU compliant.

jetty-distribution/src/main/resources/bin/jetty.sh

@@ -6,7 +6,7 @@
 # Set the name which is used by other variables.
 # Defaults to the file name without extension.
 ##################################################
-NAME=$(echo $(basename $0) | sed -e 's/^[SK][0-9]+//' -e 's/\.sh$//')
+NAME=$(echo $(basename $0) | sed -e 's/^[SK][0-9]*//' -e 's/\.sh$//')
 
 # To get the service to restart correctly on reboot, uncomment below (3 lines):
 # ========================