# HG changeset patch
# User wenzelm
# Date 1631527091 -7200
# Node ID de4b3abaf3ca41130a5a4d52479f57ee0072d747
# Parent  a117c076aa2267294f4792a871e4da2a2a9e55c8
tuned;

diff -r a117c076aa22 -r de4b3abaf3ca src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Sep 13 11:52:32 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Sep 13 11:58:11 2021 +0200
@@ -345,7 +345,7 @@
   def exit(): Unit =
   {
     log("\n")
-    sys.exit(if (session_.value.isDefined) Process_Result.RC.failure else Process_Result.RC.ok)
+    sys.exit(if (session_.value.isEmpty) Process_Result.RC.ok else Process_Result.RC.failure)
   }