# HG changeset patch
# User wenzelm
# Date 1368528386 -7200
# Node ID fe16d1128a14857b47f355487a59328efe65746b
# Parent  4f3a5f4c1169fd0e39a1c49174a68ac5ca4da868
support for more informative crashes;

diff -r 4f3a5f4c1169 -r fe16d1128a14 src/Pure/System/command_line.scala
--- 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)
   }
 }