fix(gui): allow html in JVariable to render renaming of variables correctly (#1769)(PR #1770)

2023-01-27 19:03:43 +02:00
parent 87b9ff3c35
commit 2d149e9a5d
1 changed files with 5 additions and 0 deletions
@@ -61,6 +61,11 @@ public class JVariable extends JNode {
 		return UiUtils.typeFormatHtml(var.getName(), var.getType());
 	}

+	@Override
+	public boolean disableHtml() {
+		return false;
+	}
+
 	@Override
 	public String getTooltip() {
 		String name = var.getName() + " (r" + var.getReg() + "v" + var.getSsa() + ")";