Use <input type=button ...> instead of <div ...> tags for the word magnets. This should make them clickable in more browsers and could improve layout.

1 files changed, 4 insertions, 3 deletions

diff --git a/src/runtime/javascript/minibar/minibar.js b/src/runtime/javascript/minibar/minibar.js
index 0af966fe1..133f1aafa 100644
--- a/src/runtime/javascript/minibar/minibar.js
+++ b/src/runtime/javascript/minibar/minibar.js
@@ -241,9 +241,10 @@ function get_completions(menu) {
 }
 
 function word(s) {
-  var w=div_class("word",text(s));
-  w.setAttribute("onclick",'add_word("'+s+'")');
-  return w;
+  //var w=div_class("word",text(s));
+  //w.setAttribute("onclick",'add_word("'+s+'")');
+  //return w;
+  return button(s,'add_word("'+s+'")');
 }
 
 function add_word1(menu,s) {