remove more flags #208

leanprover-community · Apr 19, 2024 · a1b1a33 · a1b1a33
1 parent 02978a3
commit a1b1a33
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
@@ -66,14 +66,17 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
         <td>{t("Levels")}</td>
         <td>{data.levels}</td>
       </tr>
-      <tr>
+      <tr className="languages">
         <td>{t("Language")}</td>
 
         <td>
           {data.languages.map((lang) => {
             let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang)
-            return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
-
+            if (lean4gameConfig.useFlags) {
+              return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
+            } else {
+              return <span title={langOpt?.name}>{lang}</span>
+            }
           })}
         </td>
       </tr>

diff --git a/client/src/css/landing_page.css b/client/src/css/landing_page.css
@@ -231,3 +231,7 @@ footer .link {
     margin-right: calc(50% - 650px);
   }
 }
+
+.info .languages span + span {
+  margin-left: .5em;
+}