# HG changeset patch
# User wenzelm
# Date 1316964334 -7200
# Node ID dd803d319d5b23e97c3894fcc5e91e0f0071c651
# Parent  6c66e268f8eb35bb2178460f03ae0e6856de0b8c
tuned signature;

diff -r 6c66e268f8eb -r dd803d319d5b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Sep 25 13:48:59 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Sep 25 17:25:34 2011 +0200
@@ -469,9 +469,11 @@
 
   /* actions */
 
-  def start(timeout: Time = Time.seconds(25), use_socket: Boolean = false, args: List[String])
+  def start(timeout: Time, use_socket: Boolean, args: List[String])
   { session_actor ! Start(timeout, use_socket, args) }
 
+  def start(args: List[String]) { start (Time.seconds(25), false, args) }
+
   def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
 
   def cancel_execution() { session_actor ! Cancel_Execution }