Review Request #1558 — Created April 30, 2010 and discarded
devserver.sh now takes a -p PORT argument to set a custom server port. If -p is not specified, defaults to 8080.
Since we're making this more complex, maybe it's time to just rewrite this in Python? It'd have the advantage of being usable to Windows users as well. You certainly don't have to do this, but it'd be a nice change.