--- 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) }
})
}
--- 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)
})
}
--- 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)
--- 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)
}