mirror of
https://github.com/jetty/jetty.project.git
synced 2025-02-23 07:37:55 +00:00
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.