diff options
| author | hallgren <hallgren@chalmers.se> | 2010-10-28 11:53:50 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2010-10-28 11:53:50 +0000 |
| commit | 7fac5dc08950da09acefc52420f7af1eb212a7c9 (patch) | |
| tree | d8c74ce33fe8fcff09fc86f942a6ecb9e56b1c02 /src/runtime/javascript/minibar | |
| parent | 119f7bc78ac60a44a579b1753f2f3f20527118cd (diff) | |
minibar.js: bug fix: the To: menu wasn't updated properly when switching grammars
Diffstat (limited to 'src/runtime/javascript/minibar')
| -rw-r--r-- | src/runtime/javascript/minibar/minibar.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/runtime/javascript/minibar/minibar.js b/src/runtime/javascript/minibar/minibar.js index b96d7c56b..a2904823b 100644 --- a/src/runtime/javascript/minibar/minibar.js +++ b/src/runtime/javascript/minibar/minibar.js @@ -102,7 +102,7 @@ function start_minibar(server,opts,target) { set_initial_language(options,menu,grammar) to_menu.onchange=get_translations - to_menu.innerHMTL=""; + to_menu.innerHTML=""; to_menu.appendChild(option("All","-1")); for(var i=0; i<lang.length; i++) if(!hasPrefix(lang[i].name,"Disamb")) |