Make tab width 2 spaces (#445)

This commit is contained in:
Francesco Stasi
2021-07-09 10:14:42 +02:00
committed by GitHub
parent 40a73af82b
commit e10f0f1683
205 changed files with 19676 additions and 20141 deletions

View File

@@ -1,19 +1,19 @@
import * as psTree from 'ps-tree';
const kill = require('tree-kill');
const [theiaPid, daemonPid] = process.argv
.slice(2)
.map((id) => Number.parseInt(id, 10));
.slice(2)
.map((id) => Number.parseInt(id, 10));
setInterval(() => {
try {
// Throws an exception if the Theia process doesn't exist anymore.
process.kill(theiaPid, 0);
} catch {
psTree(daemonPid, function (_, children) {
for (const { PID } of children) {
kill(PID);
}
kill(daemonPid, () => process.exit());
});
}
try {
// Throws an exception if the Theia process doesn't exist anymore.
process.kill(theiaPid, 0);
} catch {
psTree(daemonPid, function (_, children) {
for (const { PID } of children) {
kill(PID);
}
kill(daemonPid, () => process.exit());
});
}
}, 1000);