src/Pure/ML-Systems/smlnj-0.93.ML
changeset 4428 5c26253b8a2e
parent 4340 f5d7fbb73103
child 4494 7e5611945959
equal deleted inserted replaced
4427:6d4545f809e5 4428:5c26253b8a2e
   137   fun getenv var = drop_last_char
   137   fun getenv var = drop_last_char
   138     (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
   138     (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
   139 end;
   139 end;
   140 
   140 
   141 
   141 
   142 (* non-ASCII input (see also Thy/symbol_input.ML) *)
   142 (* non-ASCII input (see also Thy/use.ML) *)
   143 
   143 
   144 val needs_filtered_use = false;
   144 val needs_filtered_use = false;