Fix name of deleted host.

diff --git a/tools/copy_host.ml b/tools/copy_host.ml
index fd98c8c..a2c1bc4 100644 (file)
--- a/tools/copy_host.ml
+++ b/tools/copy_host.ml
@@ -3,7 +3,7 @@
  *
  * Use 'copy_host --help' for usage.
  *
- * $Id: copy_host.ml,v 1.4 2006/12/11 15:28:50 rich Exp $
+ * $Id: copy_host.ml,v 1.5 2006/12/11 15:34:36 rich Exp $
  *)
 
 open Printf
@@ -394,7 +394,7 @@ let () =
   if dhost_exists then (
     if overwrite then (
       (* Rename the destination host. *)
-      let name = sprintf "deleted-%g" (Unix.time ()) in
+      let name = sprintf "deleted-%.0f" (Unix.time ()) in
 
       printf "Renaming old host %s to %s\n%!" dcanonical_hostname name;