# HG changeset patch
# User wenzelm
# Date 1203176640 -3600
# Node ID ea11278a0300cd69057ec8987c73d7a23f3e1b82
# Parent  fbdb1161b4b0b6ad3934172ba80415f584391cba
removed managed_process (cf. General/shell_process.ML);

diff -r fbdb1161b4b0 -r ea11278a0300 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:43:59 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:44:00 2008 +0100
@@ -19,7 +19,6 @@
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
-  val managed_process: string -> string * bool
   val self_critical: unit -> bool
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
@@ -42,12 +41,6 @@
 fun max_threads_value () = Int.max (! max_threads, 1);
 
 
-(* managed external processes *)
-
-fun managed_process _ =
-  raise Fail "No multithreading support -- cannot manage external processes";
-
-
 (* critical section *)
 
 fun self_critical () = false;