# HG changeset patch
# User wenzelm
# Date 1204834391 -3600
# Node ID 58790194116c796a806344706b2a84e9c4f27fcb
# Parent  7ddf8a34dbd5d4911078f730433d17f0af93c8f7
added dummy version of string_of_pid;

diff -r 7ddf8a34dbd5 -r 58790194116c src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Thu Mar 06 21:08:20 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML	Thu Mar 06 21:13:11 2008 +0100
@@ -192,6 +192,8 @@
   end;
 end;
 
+fun string_of_pid _ = raise Fail "string_of_pid undefined";
+
 fun getenv var =
   (case OS.Process.getEnv var of
     NONE => ""