1 files changed, 1 insertions, 1 deletions

diff --git a/docs/repl.js b/docs/repl.js
index cf7a9071..fc097829 100644
--- a/docs/repl.js
+++ b/docs/repl.js
@@ -129,7 +129,7 @@ let setPrefix = () => {
     let c = Array.from(d)[1];
     let t = d.slice(1+c.length).replace(';','\n');
     let k = revkeys[c]; if (k) t += '\n'+prefix+(k==='"'?'"':k);
-    x.hashelp = i < 64;
+    x.hashelp = i < 64; // comment out after patch for double struck
     x.title = primhelp[c] = t;
   });
 }