tuned signature;
authorwenzelm
Sun Sep 25 17:25:34 2011 +0200 (2011-09-25 ago)
changeset 45076dd803d319d5b
parent 45075 6c66e268f8eb
child 45077 3cb902212af5
tuned signature;
src/Pure/System/session.scala
     1.1 --- a/src/Pure/System/session.scala	Sun Sep 25 13:48:59 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Sep 25 17:25:34 2011 +0200
     1.3 @@ -469,9 +469,11 @@
     1.4  
     1.5    /* actions */
     1.6  
     1.7 -  def start(timeout: Time = Time.seconds(25), use_socket: Boolean = false, args: List[String])
     1.8 +  def start(timeout: Time, use_socket: Boolean, args: List[String])
     1.9    { session_actor ! Start(timeout, use_socket, args) }
    1.10  
    1.11 +  def start(args: List[String]) { start (Time.seconds(25), false, args) }
    1.12 +
    1.13    def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
    1.14  
    1.15    def cancel_execution() { session_actor ! Cancel_Execution }