changeset 41491 | a2ad5b824051 |
parent 33823 | 24090eae50b6 |
child 43703 | c37a1f29bbc0 |
--- a/src/Tools/WWW_Find/socket_util.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/socket_util.ML Mon Jan 10 15:45:46 2011 +0100 @@ -41,7 +41,7 @@ val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock); val sock_name = - String.concat [ NetHostDB.toString haddr, ":", Int.toString port ]; + String.concat [ NetHostDB.toString haddr, ":", string_of_int port ]; val rd = BinPrimIO.RD {