Some work on minibar:

1. Menu for choosing target language.
2. Pass options when calling start_minibar.
See about.html for more details.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/runtime/javascript/minibar/support.js b/src/runtime/javascript/minibar/support.js
index cd1618a63..f124d5194 100644
--- a/src/runtime/javascript/minibar/support.js
+++ b/src/runtime/javascript/minibar/support.js
@@ -74,6 +74,12 @@ function button(label,action) {
   return el;
 }
 
+function option(label,value) {
+    var el=empty("option","value",value);
+    el.innerHTML=label;
+    return el;
+}
+
 function appendChildren(el,cs) {
   for(var i=0;i<cs.length;i++)
     el.appendChild(cs[i]);