diff options
Diffstat (limited to 'docs/repl.js')
| -rw-r--r-- | docs/repl.js | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/docs/repl.js b/docs/repl.js index fc097829..2bd7d117 100644 --- a/docs/repl.js +++ b/docs/repl.js @@ -129,7 +129,6 @@ 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; // comment out after patch for double struck x.title = primhelp[c] = t; }); } @@ -138,9 +137,9 @@ doc.kb.onmousedown = ev => { let t = ev.target; if (t.nodeName === 'SPAN') { if (ev.button || modified(ev)) { - let name = t.title.toLowerCase().replace(/ |\n\\.*/g,'') + let name = t.title.toLowerCase().replace(/ (\(.*)?|\n\\.*/g,'') .replace(/[\n/]/g,'_'); - if (t.hashelp) window.open('help/'+name+'.html'); + window.open('help/'+name+'.html'); return false; } else { return typeChar(doc.code, t.textContent, ev); |