# HG changeset patch
# User Nicholas Jillings <n.g.r.jillings@se14.qmul.ac.uk>
# Date 1450882101 0
# Node ID 8bf6395cefc10a80e179a8406a2a5a24976973b7
# Parent  f9c9a40f33bd8c1ba93b98b5e11463f04a7655ed
Version 1.1.0

diff -r f9c9a40f33bd -r 8bf6395cefc1 core.js
--- a/core.js	Wed Dec 23 14:36:00 2015 +0000
+++ b/core.js	Wed Dec 23 14:48:21 2015 +0000
@@ -399,7 +399,7 @@
 			for (var i=0; i<node.options.length; i++) {
 				var option = node.options[i];
 				var input = document.createElement('input');
-				input.id = option.id;
+				input.id = option.name;
 				input.type = 'checkbox';
 				var span = document.createElement('span');
 				span.textContent = option.text;
@@ -1779,8 +1779,13 @@
 								this.statement = element.textContent;
 							} else if (element.nodeName == 'option') {
 								var node = new this.childOption();
-								node.id = element.id;
-								node.name = element.getAttribute('name');
+								if (element.getAttribute('id') != null)
+								{
+									console.log('Checkbox Option id is deprecated, use name instead');
+									node.name = element.getAttribute('id');
+								} else {
+									node.name = element.getAttribute('name');
+								}
 								node.text = element.textContent;
 								this.options.push(node);
 							}
@@ -1827,7 +1832,7 @@
 					{
 						var option = this.options[i];
 						var optionNode = root.createElement("option");
-						optionNode.id = option.id;
+						optionNode.setAttribute("name",option.name);
 						optionNode.textContent = option.text;
 						node.appendChild(optionNode);
 					}