Skip to content

Commit

Permalink
Export LocationsContext in @leanprover/infoview (#379)
Browse files Browse the repository at this point in the history
The `LocationsContext` is exported in `infoview/goalLocation.tsx` but not in the `.index.tsx` file.
  • Loading branch information
0art0 authored Feb 17, 2024
1 parent 8246499 commit cd0968f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lean4-infoview/src/index.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ export { EditorContext, VersionContext } from './infoview/contexts';
export { EditorConnection } from './infoview/editorConnection';
export { RpcContext } from './infoview/rpcSessions';
export { ServerVersion } from './infoview/serverVersion';
export { GoalLocation, GoalsLocation } from './infoview/goalLocation';
export { LocationsContext, GoalLocation, GoalsLocation } from './infoview/goalLocation';
export { importWidgetModule, DynamicComponent, DynamicComponentProps,
PanelWidgetProps } from './infoview/userWidget';

Expand Down

0 comments on commit cd0968f

Please sign in to comment.