From 1ff6d92b1760f56904c4b198979446eee383e412 Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Wed, 26 May 2010 11:47:15 +0000
Subject: [PATCH] Use <input type=button ...> instead of <div ...> tags for the
 word magnets. This should make them clickable in more browsers and could
 improve layout.

---
 src/runtime/javascript/minibar/minibar.js | 7 ++++---
 1 file 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) {