From c7916ff49ceee3d22802e5b34efcde32bfe3bbe9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jens=20M=C3=B6nig?= Date: Thu, 27 Jan 2022 23:51:28 +0100 Subject: [PATCH] Update gui.js --- src/gui.js | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/gui.js b/src/gui.js index 75bf3182..2abd1ece 100644 --- a/src/gui.js +++ b/src/gui.js @@ -1764,6 +1764,7 @@ IDE_Morph.prototype.createSpriteBar = function () { // tab bar tabBar.tabTo = function (tabString) { var active; + if (myself.currentTab === tabString) {return; } myself.world().hand.destroyTemporaries(); myself.currentTab = tabString; this.children.forEach(each => { @@ -1917,7 +1918,7 @@ IDE_Morph.prototype.createSpriteEditor = function () { this.add(this.spriteEditor); } - this.spriteEditor.contents.mouseEnterDragging = (morph) => { + this.spriteEditor.mouseEnterDragging = (morph) => { if (morph instanceof BlockMorph) { this.spriteBar.tabBar.tabTo('scripts'); } else if (morph instanceof CostumeIconMorph) { @@ -1926,6 +1927,9 @@ IDE_Morph.prototype.createSpriteEditor = function () { this.spriteBar.tabBar.tabTo('sounds'); } }; + + this.spriteEditor.contents.mouseEnterDragging = + this.spriteEditor.mouseEnterDragging; }; IDE_Morph.prototype.createCorralBar = function () {