# HG changeset patch
# User clasohm
# Date 821713676 -3600
# Node ID 88b73ad6b0daf6a80ced4a73665f0060c498da2f
# Parent  aefcd255ed4a3e3e9532b1f03c6b6e0b66cae3fa
fixed bug in file_info

diff -r aefcd255ed4a -r 88b73ad6b0da src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Thu Jan 11 10:29:31 1996 +0100
+++ b/src/Pure/POLY.ML	Mon Jan 15 14:47:56 1996 +0100
@@ -60,7 +60,18 @@
 (*Get a string containing the time of last modification, attributes, owner
   and size of file (but not the path) *)
 fun file_info "" = ""
-  | file_info name = string_of_int (System.filedate name);
+  | file_info name =
+    let fun radixpand num : int list =
+          let fun radix (n, tail) =
+            if n < 10 then n :: tail
+            else radix (n div 10, (n mod 10) :: tail)
+          in radix (num, []) end;
+
+        fun radixstring num =
+          let val offset = ord "0";
+              fun chrof n = chr (offset + n);
+          in implode (map chrof (radixpand num)) end;
+     in radixstring (System.filedate name) end;
 
 (*Delete a file *)
 fun delete_file name =