--- a/src/Pure/System/command_line.scala Tue May 14 12:31:11 2013 +0200
+++ b/src/Pure/System/command_line.scala Tue May 14 12:46:26 2013 +0200
@@ -21,11 +21,18 @@
def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
}
+ var debug = false
+
def tool(body: => Int): Nothing =
{
val rc =
try { body }
- catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
+ catch {
+ case exn: Throwable =>
+ if (debug) exn.printStackTrace
+ java.lang.System.err.println(Exn.message(exn))
+ 2
+ }
sys.exit(rc)
}
}