Skip to content

Commit 515f072

Browse files
authored
Merge branch 'master' into sw/fix-wrappers
2 parents 6c7bf15 + c2cdc7a commit 515f072

File tree

3 files changed

+9
-5
lines changed

3 files changed

+9
-5
lines changed

media/programflow-visualization/webview.css

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,3 +192,7 @@ body {
192192
.traceback-text {
193193
color: red;
194194
}
195+
196+
#bottom-area button {
197+
line-height: 18px;
198+
}

src/extension.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ export function activate(context: vscode.ExtensionContext) {
364364
vscode.window.showWarningMessage('Not a python file');
365365
return;
366366
}
367-
vscode.window.activeTextEditor?.document.save();
367+
await vscode.window.activeTextEditor?.document.save();
368368
const pyCmd = getPythonCmd(pyExt);
369369
let verboseOpt = "";
370370
if (isDebug(context)) {

src/programflow-visualization/frontend/visualization_panel.ts

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -169,10 +169,10 @@ export class VisualizationPanel {
169169
<p id="traceMax">/?</p>
170170
</div>
171171
<div class="row margin-vertical">
172-
<button class="margin-horizontal" id="firstButton" type="button" onclick="onClick('first')">First</button>
173-
<button class="margin-horizontal" id="prevButton" type="button" onclick="onClick('prev')">Prev</button>
174-
<button class="margin-horizontal" id="nextButton" type="button" onclick="onClick('next')">Next</button>
175-
<button class="margin-horizontal" id="lastButton" type="button" onclick="onClick('last')">Last</button>
172+
<button class="margin-horizontal" id="firstButton" type="button" onclick="onClick('first')">&#9198</button>
173+
<button class="margin-horizontal" id="prevButton" type="button" onclick="onClick('prev')">&#9664</button>
174+
<button class="margin-horizontal" id="nextButton" type="button" onclick="onClick('next')">&#9654</button>
175+
<button class="margin-horizontal" id="lastButton" type="button" onclick="onClick('last')">&#9197</button>
176176
</div>
177177
</div>
178178
<div class="column floating-right">

0 commit comments

Comments
 (0)