changeset 73 | 075db6ac7f2f |
parent 66 | 1b14cd923772 |
child 100 | e95b98536b3d |
72:099d949fe467 | 73:075db6ac7f2f |
---|---|
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); |
93 fun delete_file name = |
94 let val _ = System.system ("rm " ^ name) |
|
95 in () end; |
|
94 |
96 |