Custom font selection (#226)

This commit is contained in:
Gregory Schier
2025-06-08 22:48:27 -07:00
committed by GitHub
parent e0aaa33ccb
commit 9fab37fb17
25 changed files with 399 additions and 56 deletions

View File

@@ -62,7 +62,7 @@ export type ProxySetting = { "type": "enabled", disabled: boolean, http: string,
export type ProxySettingAuth = { user: string, password: string, };
export type Settings = { model: "settings", id: string, createdAt: string, updatedAt: string, appearance: string, editorFontSize: number, editorSoftWrap: boolean, hideWindowControls: boolean, interfaceFontSize: number, interfaceScale: number, openWorkspaceNewWindow: boolean | null, proxy: ProxySetting | null, themeDark: string, themeLight: string, updateChannel: string, editorKeymap: EditorKeymap, coloredMethods: boolean, };
export type Settings = { model: "settings", id: string, createdAt: string, updatedAt: string, appearance: string, coloredMethods: boolean, editorFont: string | null, editorFontSize: number, editorKeymap: EditorKeymap, editorSoftWrap: boolean, hideWindowControls: boolean, interfaceFont: string | null, interfaceFontSize: number, interfaceScale: number, openWorkspaceNewWindow: boolean | null, proxy: ProxySetting | null, themeDark: string, themeLight: string, updateChannel: string, };
export type SyncState = { model: "sync_state", id: string, workspaceId: string, createdAt: string, updatedAt: string, flushedAt: string, modelId: string, checksum: string, relPath: string, syncDir: string, };