# HG changeset patch
# User wenzelm
# Date 1537619093 -7200
# Node ID c5db368833b1c1a4d0a1e2960d674d7df1ef85cb
# Parent  90bb4cabe1e870ef55d58dd8f86d04afaeb3fda0
proper return code for runtime failure;

diff -r 90bb4cabe1e8 -r c5db368833b1 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sat Sep 22 13:22:43 2018 +0200
+++ b/src/Pure/Thy/present.scala	Sat Sep 22 14:24:53 2018 +0200
@@ -319,6 +319,6 @@
       build_document(document_dir = document_dir, document_name = document_name,
         document_format = document_format, tags = tags)
     }
-    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
+    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) }
   })
 }
diff -r 90bb4cabe1e8 -r c5db368833b1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Sep 22 13:22:43 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 22 14:24:53 2018 +0200
@@ -270,6 +270,6 @@
               sessions = sessions))
         }
 
-      if (!ok) sys.exit(1)
+      if (!ok) sys.exit(2)
     })
 }
diff -r 90bb4cabe1e8 -r c5db368833b1 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Sep 22 13:22:43 2018 +0200
+++ b/src/Pure/Tools/server.scala	Sat Sep 22 14:24:53 2018 +0200
@@ -485,7 +485,7 @@
       }
       else if (operation_exit) {
         val ok = Server.exit(name)
-        sys.exit(if (ok) 0 else 1)
+        sys.exit(if (ok) 0 else 2)
       }
       else {
         val log = Logger.make(log_file)
diff -r 90bb4cabe1e8 -r c5db368833b1 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Sep 22 13:22:43 2018 +0200
+++ b/src/Tools/VSCode/src/server.scala	Sat Sep 22 14:24:53 2018 +0200
@@ -361,7 +361,7 @@
 
   def exit() {
     log("\n")
-    sys.exit(if (session_.value.isDefined) 1 else 0)
+    sys.exit(if (session_.value.isDefined) 2 else 0)
   }