aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJeremy Rifkin <51220084+jeremy-rifkin@users.noreply.github.com>2022-05-15 20:40:11 -0400
committerJeremy Rifkin <51220084+jeremy-rifkin@users.noreply.github.com>2022-05-15 20:40:11 -0400
commit3603b08b8f9a44690966c0e1f852042e545dab41 (patch)
treeaf827fa8b22890418dbea087f297b1edb811da87
parenta508243c2dff6b1a5a5d333500e6b5d77a9224f7 (diff)
downloadcompiler-explorer-gh-2938.tar.gz
compiler-explorer-gh-2938.zip
Fix and clarification, thanks Rubengh-2938
-rw-r--r--static/settings.ts8
1 files changed, 4 insertions, 4 deletions
diff --git a/static/settings.ts b/static/settings.ts
index 14f758e34..4659f07aa 100644
--- a/static/settings.ts
+++ b/static/settings.ts
@@ -50,7 +50,7 @@ export interface SiteSettings {
enableCtrlStree: boolean;
editorsFFont: string;
editorsFLigatures: boolean;
- defaultFontScale?: number;
+ defaultFontScale?: number; // the font scale widget can check this setting before the default has been populated
formatBase: FormatBase;
formatOnCompile: boolean;
hoverShowAsmDoc: boolean;
@@ -279,7 +279,7 @@ export class Settings {
selector: string,
name: keyof SiteSettings,
populate: {label: string; desc: string}[],
- defaultValue: string,
+ defaultValue: any,
component = Select
) => {
this.add(new component(this.root.find(selector), name, populate), defaultValue);
@@ -316,12 +316,12 @@ export class Settings {
.css('cursor', 'not-allowed');
}
- const defaultFontSize = this.settings.defaultFontScale || options.defaultFontScale;
+ const defaultFontScale = options.defaultFontScale;
const fontScales: {label: string; desc: string}[] = [];
for (let i = 8; i <= 30; i++) {
fontScales.push({label: i.toString(), desc: i.toString()});
}
- addSelector('.defaultFontScale', 'defaultFontScale', fontScales, defaultFontSize.toString(), NumericSelect);
+ addSelector('.defaultFontScale', 'defaultFontScale', fontScales, defaultFontScale, NumericSelect);
const formats: FormatBase[] = ['Google', 'LLVM', 'Mozilla', 'Chromium', 'WebKit', 'Microsoft', 'GNU'];
const formatsData = formats.map(format => {