From f462bcac9ccbd2b52acc0ca533fb8751550059e9 Mon Sep 17 00:00:00 2001
From: Sashko Stubailo <sashko@mit.edu>
Date: Mon, 12 Jan 2015 11:53:37 -0800
Subject: [PATCH] Add comment explaining named pipe naming

---
 tools/server/shell.js | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/server/shell.js b/tools/server/shell.js
index 0b6ce7c36d..9e3ae23ca5 100644
--- a/tools/server/shell.js
+++ b/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, "_");
   }