Skip to content

Commit

Permalink
fix/ReopenGoalsPan: remove redundant check on info panel
Browse files Browse the repository at this point in the history
  • Loading branch information
Alidra committed Mar 19, 2024
1 parent 63471e1 commit de5a132
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions editors/vscode/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -535,12 +535,8 @@ function refreshGoals(panel: WebviewPanel | null | undefined, editor: TextEditor
panel = context.workspaceState.get('panel')!;
}


if (panel != null) {
const styleUri = panel!.webview.asWebviewUri(Uri.joinPath(context.extensionUri, 'media', 'styles.css'))
sendGoalsRequest(proofState, panel!, editor.document.uri, styleUri);
} else {
}
const styleUri = panel!.webview.asWebviewUri(Uri.joinPath(context.extensionUri, 'media', 'styles.css'))
sendGoalsRequest(proofState, panel!, editor.document.uri, styleUri);
}

// returns the HTML code of goals environment
Expand Down

0 comments on commit de5a132

Please sign in to comment.