add config option to disable flags in preferences #208

leanprover-community · Apr 18, 2024 · 8cf358e · 8cf358e
1 parent 3ddcc35
commit 8cf358e
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx
@@ -16,6 +16,8 @@ export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
   let { t } = useTranslation()
   const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
 
+
+
   const marks = [
     {
       value: 0,
@@ -59,7 +61,13 @@ export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
                     value={language}
                     label={t("Language")}
                     onChange={handlerChangeLanguage}>
-                      {lean4gameConfig.languages.map(lang => {return <MenuItem key={`menu-item-lang-${lang.iso}`} value={lang.iso}><ReactCountryFlag countryCode={lang.flag}/>&nbsp;{lang.name}</MenuItem>})}
+                      {lean4gameConfig.languages.map(lang => {
+                        return <MenuItem key={`menu-item-lang-${lang.iso}`} value={lang.iso}>
+                          {lean4gameConfig.useFlags && <ReactCountryFlag countryCode={lang.flag}/>}
+                          &nbsp;
+                          {lang.name}
+                        </MenuItem>
+                      })}
                   </Select>
                 </Box>
               }

diff --git a/client/src/config.json b/client/src/config.json
@@ -22,5 +22,6 @@
       "flag": "CN",
       "name": "中文"
     }
-  ]
+  ],
+  "useFlags": false
 }