Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
BelegCuthalion authored May 29, 2019
1 parent 61be3d7 commit 807872a
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions client/src/CoqDocument.ts
Original file line number Diff line number Diff line change
Expand Up @@ -176,9 +176,9 @@ export class CoqDocument implements vscode.Disposable {
this.project.infoOut.appendLine(psm.prettyTextToString(params.message));
return;
case 'notice':
this.project.noticeOut.clear();
this.project.noticeOut.show(true);
this.project.noticeOut.append(psm.prettyTextToString(params.message));
this.project.noticeOut.append("\n");
return;
// vscode.window.showInformationMessage(params.message); return;
// case 'error':
Expand Down Expand Up @@ -550,4 +550,4 @@ export class CoqDocument implements vscode.Disposable {
return this.focus;
}

}
}

0 comments on commit 807872a

Please sign in to comment.