Thank you for that. That looks good, simpler than using an extra grep. I've not seen those sed options before.

One minor suggestion, it might be worth changing:
proxyport=$(echo $http_proxy | sed -n 's?http://[^:]\+:\([0-9]\+\)?\1?p')
proxyport=$(echo $http_proxy | sed -n 's?http://[^:]\+:\([0-9]\+\).*?\1?p')

It might not be necessary, but just in case the http_proxy is incorrectly set with an extra / or something after the port number, then the extra ".*" will catch and remove it.

Pkg-grass-devel mailing list

Reply via email to