From 12957d774054ec73d2875e5b159b4f617993b3f3 Mon Sep 17 00:00:00 2001 From: Steven Hugg Date: Tue, 14 Nov 2023 10:57:19 -0600 Subject: [PATCH] changed file selector to --- src/ide/ui.ts | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/ide/ui.ts b/src/ide/ui.ts index 6711cedd..804d925f 100644 --- a/src/ide/ui.ts +++ b/src/ide/ui.ts @@ -1220,13 +1220,13 @@ async function _downloadAllFilesZipFile(e) { } function populateExamples(sel) { - var files = {}; - sel.append($("").attr('label','Examples').appendTo(sel); for (var i=0; i").val(preset.id).text(name).attr('selected',isCurrentPreset?'selected':null)); + optgroup.append($("").attr('label','Repositories').appendTo(sel); for (let repopath in repos) { var repo = repos[repopath]; if (repo.platform_id && getBasePlatform(repo.platform_id) == getBasePlatform(platform_id)) { - if (n++ == 0) - sel.append($("").attr('label',category).appendTo(sel); + let name = key.substring(prefix.length); + optgroup.append($("