if firefox then 18px font-size else 16px

JMU-CS · Jul 22, 2024 · eda87ff · eda87ff
1 parent 125bd20
commit eda87ff
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/common.js b/src/common.js
@@ -282,8 +282,11 @@ export function getStopClicked() {
     return stopClicked;
 }
 
+const isFirefox = navigator.userAgent.toLowerCase().includes('firefox');
+const fontSize = isFirefox ? 18 : 16;
+
 export const textEditor = ace.edit("aceCode", {
-  fontSize: 18,
+  fontSize: fontSize,
   mode: 'ace/mode/praxly',
 });