equal
deleted
inserted
replaced
77 result |
77 result |
78 end |
78 end |
79 else f(); |
79 else f(); |
80 |
80 |
81 |
81 |
82 (*** File information ***) |
82 (*** File handling ***) |
83 |
83 |
84 (*Get time of last modification.*) |
84 (*Get time of last modification.*) |
85 local |
85 local |
86 open System.Timer; |
86 open System.Timer; |
87 open System.Unsafe.SysIO; |
87 open System.Unsafe.SysIO; |
88 in |
88 in |
89 fun file_info "" = "" |
89 fun file_info "" = "" |
90 | file_info name = makestring (mtime (PATH name)); |
90 | file_info name = makestring (mtime (PATH name)); |
91 end; |
91 end; |
92 |
92 |
|
93 fun delete_file name = System.system ("rm " ^ name); |
|
94 |