diff options
| -rw-r--r-- | src/www/minibar/minibar.js | 8 | ||||
| -rw-r--r-- | src/www/minibar/minibar_online.js | 2 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js index 6822e7926..944d4d93b 100644 --- a/src/www/minibar/minibar.js +++ b/src/www/minibar/minibar.js @@ -220,7 +220,7 @@ Minibar.prototype.get_pgf_info=function() { Minibar.prototype.show_pgf_info=function(info) { var t=this; var cnt=0; - console.log(info) + //console.log(info) info=info.split("\n"); for(var i=0;i<info.length;i++) { if(info[i]=="") info[i]="<p>" @@ -270,6 +270,12 @@ Minibar.prototype.show_grammarinfo=function() { var info=empty("div") if(t.pgf_info) info.innerHTML=t.pgf_info + if(true || /^\/(tmp|grammars)\//.test(server.grammars_url)) { + var q="?"+server.grammars_url+" "+server.current_grammar_url + var link=node("a",{href:q}) + link.appendChild(text(link.href)); + info.appendChild(wrap("p",[text("Link directly to this grammar: "),link])) + } clear(t.translations.main) var hdr=[text(g.name)] diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js index 8ff10f7fb..0d7792e9d 100644 --- a/src/www/minibar/minibar_online.js +++ b/src/www/minibar/minibar_online.js @@ -21,7 +21,7 @@ var minibar_options= { try_google: true } -if(/^\?\/tmp\//.test(location.search)) { +if(/^\?\/(tmp|grammars)\//.test(location.search)) { var args=decodeURIComponent(location.search.substr(1)).split(" ") if(args[0]) online_options.grammars_url=args[0]; if(args[1]) minibar_options.initial_grammar=args[1]; |