Update gui.js

jmoenig · Aug 7, 2024 · f67f1b6 · f67f1b6
1 parent a2e8e53
commit f67f1b6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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;
             }
         );
 /*