[tor-commits] [websocket/master] Change back to "websocket" names from "pt-websocket" names.