# HG changeset patch
# User wenzelm
# Date 870794761 -7200
# Node ID 3ac6d6bcae424be284756a283042b49f1af68116
# Parent  c44c8300689192e7a2d6dcc703cde9a3d124c282
added getenv;

diff -r c44c83006891 -r 3ac6d6bcae42 src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 17:21:24 1997 +0200
+++ b/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 17:26:01 1997 +0200
@@ -108,9 +108,18 @@
   end;
 
 
-(*"false" writes an image file that is executed via the MLWorks "mlimage" 
-  script, while "true" would yield a larger, self-contained executable.*)
-fun xML filename = Shell.saveImage (filename, false);
+(* getenv *)
+
+local
+  fun drop_last [] = []
+    | drop_last [x] = []
+    | drop_last (x :: xs) = x :: drop_last xs;
+
+  val drop_last_char = implode o drop_last o explode;
+in
+  fun getenv var = drop_last_char
+    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
+end;
 
 
 (*Non-printing and 8-bit chars are forbidden in string constants*)