Merge remote-tracking branch 'origin/main' into actions_io

This commit is contained in:
Robert 2020-08-10 15:59:27 +01:00
commit 7c2a7b236c
22 changed files with 90 additions and 148 deletions

View file

@ -389,3 +389,11 @@ function getCodeQLForCmd(cmd: string): CodeQL {
}
};
}
export function isTracedLanguage(language: string): boolean {
return ['cpp', 'java', 'csharp'].includes(language);
}
export function isScannedLanguage(language: string): boolean {
return !isTracedLanguage(language);
}