changeset 51085 | d90218288d51 |
parent 45066 | 11f622794ad6 |
child 53709 | 84522727f9d3 |
--- a/src/Tools/WWW_Find/scgi_server.ML Sun Feb 10 22:07:56 2013 +0100 +++ b/src/Tools/WWW_Find/scgi_server.ML Mon Feb 11 14:39:04 2013 +0100 @@ -103,7 +103,7 @@ loop () end; in - tracing ("SCGI server started."); + tracing ("SCGI server started on port " ^ string_of_int port ^ "."); dump_handlers (); loop (); Socket.close passive_sock