# HG changeset patch # User wenzelm # Date 918148520 -3600 # Node ID 3198f547f8afc641ffa4bdc42636256e03ee70ae # Parent 42c94393d39ed1c563683fb03ea20f15b229d6cc fixed file_info; diff -r 42c94393d39e -r 3198f547f8af src/Pure/ML-Systems/mlworks.ML --- a/src/Pure/ML-Systems/mlworks.ML Thu Feb 04 18:15:01 1999 +0100 +++ b/src/Pure/ML-Systems/mlworks.ML Thu Feb 04 18:15:20 1999 +0100 @@ -124,9 +124,8 @@ (* file handling *) -(*get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" (* FIXME !? *) - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; +(*get time of last modification*) +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; (* getenv *) diff -r 42c94393d39e -r 3198f547f8af src/Pure/ML-Systems/polyml.ML --- 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 diff -r 42c94393d39e -r 3198f547f8af src/Pure/ML-Systems/smlnj-0.93.ML --- a/src/Pure/ML-Systems/smlnj-0.93.ML Thu Feb 04 18:15:01 1999 +0100 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Thu Feb 04 18:15:20 1999 +0100 @@ -174,12 +174,11 @@ (* file handling *) -(*Get time of last modification; if file doesn't exist return an empty string*) +(*get time of last modification*) local open System.Timer System.Unsafe.SysIO; in - fun file_info "" = "" - | file_info name = makestring (mtime (PATH name)) handle _ => ""; + fun file_info name = makestring (mtime (PATH name)) handle _ => ""; end; structure OS = diff -r 42c94393d39e -r 3198f547f8af src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:01 1999 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:20 1999 +0100 @@ -192,9 +192,8 @@ (* file handling *) -(*get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" (* FIXME !? *) - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; +(*get time of last modification*) +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; (* getenv *)