From c5d811523ed969c0667252e5ee8bcd9e4931e531 Mon Sep 17 00:00:00 2001 From: Bernat Romagosa Date: Mon, 11 Dec 2023 11:53:46 +0100 Subject: [PATCH] allow #open: to fetch and load libraries from a URL --- src/gui.js | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/gui.js b/src/gui.js index 4df5926b1c..98e6e53185 100644 --- a/src/gui.js +++ b/src/gui.js @@ -545,6 +545,14 @@ IDE_Morph.prototype.openIn = function (world) { projectData.indexOf('