waveterm/xterm.js
0
0
Fork 0
mirror of https://github.com/wavetermdev/xterm.js.git synced 2026-08-05 13:43:48 -07:00
Code Issues Packages Projects Releases Wiki Activity

fixes #1667

Browse Source
This commit is contained in:
Jörg Breitbart
2018-09-08 17:26:19 +02:00
parent bdb6647ae0
commit 4eede85ef6
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
demo/client.ts
+2 -2
View File
@@ -101,7 +101,7 @@ function createTerminal(): void {
if (e.key === 'Enter') {
e.preventDefault();
let searchOptions = {
regex: document.getElementById('regex').checked,
regex: (document.getElementById('regex') as HTMLInputElement).checked,
wholeWord: false,
caseSensitive: false
};
@@ -112,7 +112,7 @@ function createTerminal(): void {
if (e.key === 'Enter') {
e.preventDefault();
let searchOptions = {
regex: document.getElementById('regex').checked,
regex: (document.getElementById('regex') as HTMLInputElement).checked,
wholeWord: false,
caseSensitive: false
};