| changeset 12108 | b6f10dcde803 |
| parent 10730 | bbaa0c6ef59f |
| child 12896 | 4518acda6d93 |
--- a/src/Pure/ML-Systems/mlworks.ML Thu Nov 08 23:55:04 2001 +0100 +++ b/src/Pure/ML-Systems/mlworks.ML Thu Nov 08 23:57:22 2001 +0100 @@ -138,8 +138,3 @@ (case OS.Process.getEnv var of NONE => "" | SOME txt => txt); - - -(* non-ASCII input (see also Thy/use.ML) *) - -val needs_filtered_use = false;