src/Pure/System/command_line.scala
changeset 51980 fe16d1128a14
parent 48346 e2382bede914
child 55618 995162143ef4
--- 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)
   }
 }