From 1db711f6e290752d908a3aa54b96d053487151de Mon Sep 17 00:00:00 2001
From: Piotr Gawron <piotr.gawron@uni.lu>
Date: Thu, 29 Mar 2018 11:21:22 +0200
Subject: [PATCH] whitespace is bigger for miriam links
---
frontend-js/src/main/js/gui/leftPanel/GuiUtils.js | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/frontend-js/src/main/js/gui/leftPanel/GuiUtils.js b/frontend-js/src/main/js/gui/leftPanel/GuiUtils.js
index 267762e196..e1025958df 100644
--- a/frontend-js/src/main/js/gui/leftPanel/GuiUtils.js
+++ b/frontend-js/src/main/js/gui/leftPanel/GuiUtils.js
@@ -245,8 +245,8 @@ GuiUtils.prototype.createAnnotationList = function (annotations, options) {
}
grouppedAnnotations[annotatorClass] = grouppedAnnotations[annotatorClass].sort(function (a, b) {
- const aType = a.getType().toUpperCase();
- const bType = b.getType().toUpperCase();
+ var aType = a.getType().toUpperCase();
+ var bType = b.getType().toUpperCase();
if (aType < bType) return -1;
else if (aType > bType) return 1;
else return 0;
@@ -276,7 +276,7 @@ GuiUtils.prototype.createAnnotationList = function (annotations, options) {
}
var header = document.createElement("div");
- header.style.width = "24px";
+ header.style.width = "28px";
header.style.float = "left";
header.innerHTML = "[" + cntAnnotations + "]";
row.appendChild(header);
--
GitLab