Add comment explaining named pipe naming

tools/server/shell.js

@@ -136,6 +136,9 @@ function startREPL(options) {
 function getSocketFile(shellDir) {
   if (process.platform === "win32") {
     // Make a Windows named pipe based on the app's path
+    // Replace the colon with an underscore to avoid "C:" appearing in the pipe
+    // name, and replace slashes to avoid weird naming collisions with
+    // directories: http://stackoverflow.com/questions/3571422/can-named-pipe-names-have-backslashes
     return "\\\\.\\pipe\\" + shellDir.replace(/[:\\]/g, "_");
   }