From f67f1b676ce77ee163c6e6d67d2262103c3f8358 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jens=20M=C3=B6nig?= Date: Wed, 7 Aug 2024 16:26:49 +0200 Subject: [PATCH] Update gui.js --- src/gui.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/gui.js b/src/gui.js index b097a37d5..f35f781d4 100644 --- a/src/gui.js +++ b/src/gui.js @@ -10492,7 +10492,7 @@ LibraryImportDialogMorph.prototype.importLibrary = function () { ide.resourceURL('libraries', selectedLibrary), libraryText => { ide.droppedText(libraryText, libraryName); - this.isLoadingLibrary = true; + // this.isLoadingLibrary = true; } ); /*