added getenv;
authorwenzelm
Tue Aug 05 17:26:01 1997 +0200 (1997-08-05)
changeset 35973ac6d6bcae42
parent 3596 c44c83006891
child 3598 28b6670e415a
added getenv;
src/Pure/ML-Systems/MLWorks.ML
     1.1 --- a/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 17:21:24 1997 +0200
     1.2 +++ b/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 17:26:01 1997 +0200
     1.3 @@ -108,9 +108,18 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(*"false" writes an image file that is executed via the MLWorks "mlimage" 
     1.8 -  script, while "true" would yield a larger, self-contained executable.*)
     1.9 -fun xML filename = Shell.saveImage (filename, false);
    1.10 +(* getenv *)
    1.11 +
    1.12 +local
    1.13 +  fun drop_last [] = []
    1.14 +    | drop_last [x] = []
    1.15 +    | drop_last (x :: xs) = x :: drop_last xs;
    1.16 +
    1.17 +  val drop_last_char = implode o drop_last o explode;
    1.18 +in
    1.19 +  fun getenv var = drop_last_char
    1.20 +    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
    1.21 +end;
    1.22  
    1.23  
    1.24  (*Non-printing and 8-bit chars are forbidden in string constants*)