--- 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 }