diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 37e2fc4..f7ce27f 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -28,7 +28,7 @@ import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context'; -import { Typewriter, hasErrors, hasInteractiveErrors } from './command_line'; +import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; import { CircularProgress } from '@mui/material'; diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/typewriter.tsx similarity index 100% rename from client/src/components/infoview/command_line.tsx rename to client/src/components/infoview/typewriter.tsx diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 00e3f87..be81063 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -27,7 +27,7 @@ import { store } from '../state/store' import { Button } from './button' import Markdown from './markdown' import {InventoryPanel} from './inventory' -import { hasInteractiveErrors } from './infoview/command_line' +import { hasInteractiveErrors } from './infoview/typewriter' import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context' import { DualEditor } from './infoview/main'