From 4de5e48313ff6d85d559cb9c7acbf424986a553c Mon Sep 17 00:00:00 2001
From: Piotr Gawron <piotr.gawron@uni.lu>
Date: Mon, 30 Apr 2018 11:41:48 +0200
Subject: [PATCH] css style is assigned properly

---
 frontend-js/src/main/js/gui/topMenu/TopMenu.js | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/frontend-js/src/main/js/gui/topMenu/TopMenu.js b/frontend-js/src/main/js/gui/topMenu/TopMenu.js
index e14b2a2402..84bd3d05ae 100644
--- a/frontend-js/src/main/js/gui/topMenu/TopMenu.js
+++ b/frontend-js/src/main/js/gui/topMenu/TopMenu.js
@@ -166,9 +166,9 @@ TopMenu.prototype.init = function () {
   commentCheckbox.onclick = function () {
     ServerConnector.getSessionData(project).setShowComments(commentCheckbox.checked);
     if (commentCheckbox.checked) {
-      refreshCommentButton.style.display = 'inline';
+      $(refreshCommentButton).css("display","inline");
     } else {
-      refreshCommentButton.style.display = 'none';
+      $(refreshCommentButton).css("display","none");
     }
     return self.getMap().refreshComments().then(null, GuiConnector.alert);
   };
@@ -195,7 +195,7 @@ TopMenu.prototype.init = function () {
     showOverviewButton.onclick = function () {
       return self._overviewDialog.showOverview();
     };
-    showOverviewButton.style.display = "";
+    $(showOverviewButton).css("display","inline-block");
   }
 
   if (ServerConnector.getSessionData().getShowComments()) {
-- 
GitLab