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')
to
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
Pkg-grass-devel@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-grass-devel

Reply via email to