From 749f7645104e9511705341057758dd7aa81c003a Mon Sep 17 00:00:00 2001 From: Dimitris Kolovos Date: Mon, 17 Feb 2025 09:19:00 +0000 Subject: [PATCH] Minor ui tweaks and cleanups --- mkdocs/docs/playground/index.html | 13 +++++-------- mkdocs/docs/playground/js/DownloadDialog.js | 3 ++- mkdocs/docs/playground/js/LiveShareDialog.js | 3 ++- mkdocs/docs/playground/js/LiveShareManager.js | 15 ++++++++++----- mkdocs/docs/playground/js/OutputPanel.js | 3 ++- mkdocs/docs/playground/js/Playground.js | 3 ++- mkdocs/docs/playground/js/SettingsDialog.js | 3 ++- 7 files changed, 25 insertions(+), 18 deletions(-) diff --git a/mkdocs/docs/playground/index.html b/mkdocs/docs/playground/index.html index 92fd8e35b..9a570fce4 100644 --- a/mkdocs/docs/playground/index.html +++ b/mkdocs/docs/playground/index.html @@ -13,21 +13,18 @@
-