fix: export type

reaslab · Dec 31, 2023 · 5d25353 · 5d25353
1 parent 7541abd
commit 5d25353
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
@@ -14,7 +14,7 @@ export { RpcContext } from './infoview/rpcSessions';
 export { ServerVersion } from './infoview/serverVersion';
 export { GoalLocation, GoalsLocation } from './infoview/goalLocation';
 export { importWidgetModule, DynamicComponent, type DynamicComponentProps,
-    PanelWidgetProps } from './infoview/userWidget';
+    type PanelWidgetProps } from './infoview/userWidget';
 
 export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode';
 export { renderInfoview, mkInfoviewApi, Infoview } from './infoview/main';