Don't update the server if managed by the user

This commit is contained in:
Laurențiu Nicola 2021-01-07 16:33:00 +02:00
parent 959406aeb5
commit c547ec1cd6

View file

@ -167,6 +167,7 @@ async function bootstrapExtension(config: Config, state: PersistentState): Promi
}
return;
};
if (serverPath(config) !== null) return;
const now = Date.now();
if (config.package.releaseTag === NIGHTLY_TAG) {
@ -278,7 +279,7 @@ async function patchelf(dest: PathLike): Promise<void> {
}
async function getServer(config: Config, state: PersistentState): Promise<string | undefined> {
const explicitPath = process.env.__RA_LSP_SERVER_DEBUG ?? config.serverPath;
const explicitPath = serverPath(config);
if (explicitPath) {
if (explicitPath.startsWith("~/")) {
return os.homedir() + explicitPath.slice("~".length);
@ -351,6 +352,10 @@ async function getServer(config: Config, state: PersistentState): Promise<string
return dest;
}
function serverPath(config: Config): string | null {
return process.env.__RA_LSP_SERVER_DEBUG ?? config.serverPath;
}
async function isNixOs(): Promise<boolean> {
try {
const contents = await fs.readFile("/etc/os-release");