app: added mini to controlgroup widget

js/erp5_loader.js

@@ -970,6 +970,7 @@
    *   "property_dict": {
    *     "id": null,
    *     "class_list": null,
+   *     "mini": null
    *     "theme": null,
    *     "direction": "horizontal",
    *     "label": {
@@ -1040,7 +1041,8 @@
       "type": "div",
       "direct": {
         "className": "ui-corner-all ui-controlgroup " +
-          (spec.class_list || "") + " ui-controlgroup-" + direction
+          (spec.class_list || "") + " ui-controlgroup-" + direction +
+            (spec.mini ? " ui-mini" : "")
       },
       "attributes": {
         "data-role": "controlgroup",