add another json dictionary option

options.js

@@ -74,6 +74,12 @@ function defaults()
         default: 0,
         label: "Where to look for definitions (does not affect jmdict readings)"
     });
+    settings.push({
+        id: "normal_definitions_in_mining",
+        kind: "checkbox",
+        default: false,
+        label: "Force \"From jmdict then json\" definitions mode when mining UI is open"
+    });
     settings.push({
         id: "strict_epwing",
         kind: "checkbox",