changeset 6227 | 3198f547f8af |
parent 6042 | 0ccde2f25dd6 |
child 7114 | f1e787b90fdc |
--- a/src/Pure/ML-Systems/polyml.ML Thu Feb 04 18:15:01 1999 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Thu Feb 04 18:15:20 1999 +0100 @@ -109,9 +109,8 @@ (* file handling *) -(*get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" (* FIXME !? *) - | file_info name = Int.toString (System.filedate name) handle _ => ""; +(*get time of last modification*) +fun file_info name = Int.toString (System.filedate name) handle _ => ""; structure OS = struct