From 99d02717e2e2664fe14192f46697fdd54ec0ba74 Mon Sep 17 00:00:00 2001
From: Piotr Gawron <piotr.gawron@uni.lu>
Date: Tue, 8 Aug 2017 13:02:29 +0200
Subject: [PATCH] name of panels are not trimmed

---
 frontend-js/src/main/js/Admin.js | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/frontend-js/src/main/js/Admin.js b/frontend-js/src/main/js/Admin.js
index 2b38dec9ae..3e9e1ac630 100644
--- a/frontend-js/src/main/js/Admin.js
+++ b/frontend-js/src/main/js/Admin.js
@@ -117,9 +117,7 @@ Admin.prototype.addTab = function(params, navElement, contentElement) {
   var navLink = document.createElement("a");
   navLink.href = "#" + tabId;
   if (name !== undefined) {
-    if (name.length > 12) {
-      name = name.substring(0, 10) + "...";
-    }
+    name = name.substring(0, 10) + "...";
     navLink.innerHTML = name;
   }
   navLink.onclick = function() {
-- 
GitLab