rename plain project

leanprover-community · Dec 17, 2023 · fbb8ccf · fbb8ccf
1 parent 62d8627
commit fbb8ccf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/client/src/Settings.tsx b/client/src/Settings.tsx
@@ -133,7 +133,7 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
                     setProject(ev.target.value)
                     console.log(`set Lean project to: ${ev.target.value}`)
                     }} >
-                <option value="Webeditor">No imports</option>
+                <option value="plain">No imports</option>
                 <option value="MathlibLatest">Latest Mathlib</option>
                 <option value="DuperDemo">Latest Duper</option>
               </select>