equal
deleted
inserted
replaced
122 end; |
122 end; |
123 |
123 |
124 |
124 |
125 (* file handling *) |
125 (* file handling *) |
126 |
126 |
127 (*get time of last modification; if file doesn't exist return an empty string*) |
127 (*get time of last modification*) |
128 fun file_info "" = "" (* FIXME !? *) |
128 fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; |
129 | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; |
|
130 |
129 |
131 |
130 |
132 (* getenv *) |
131 (* getenv *) |
133 |
132 |
134 fun getenv var = |
133 fun getenv var = |