From 6d32739261be280b9556910e103c3e5e31da355f Mon Sep 17 00:00:00 2001 From: "Cornelius A. Ludmann" Date: Fri, 25 Jun 2021 08:30:11 +0000 Subject: [PATCH] [dashboard] Add Theia deprecaton warning --- components/dashboard/src/settings/Preferences.tsx | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/components/dashboard/src/settings/Preferences.tsx b/components/dashboard/src/settings/Preferences.tsx index ec5db2e44c4bee..f0b0ef8510350e 100644 --- a/components/dashboard/src/settings/Preferences.tsx +++ b/components/dashboard/src/settings/Preferences.tsx @@ -12,12 +12,13 @@ import theia from '../images/theia-gray.svg'; import vscode from '../images/vscode.svg'; import { PageWithSubMenu } from "../components/PageWithSubMenu"; import settingsMenu from "./settings-menu"; +import AlertBox from "../components/AlertBox"; type Theme = 'light' | 'dark' | 'system'; export default function Preferences() { const { user } = useContext(UserContext); - const [ defaultIde, setDefaultIde ] = useState(user?.additionalData?.ideSettings?.defaultIde || 'theia'); + const [ defaultIde, setDefaultIde ] = useState(user?.additionalData?.ideSettings?.defaultIde || 'code'); const actuallySetDefaultIde = async (value: string) => { const additionalData = user?.additionalData || {}; const settings = additionalData.ideSettings || {}; @@ -46,6 +47,9 @@ export default function Preferences() {

Default IDE

Choose which IDE you want to use.

+ + We're deprecating the Theia editor. You can still switch back to Theia for the next few weeks but the preference will be removed by the end of August 2021. +
actuallySetDefaultIde('code')}>