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.
--
To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
