src/Tools/WWW_Find/socket_util.ML
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers;
Fri, 23 Sep 2011 17:23:54 +0200 wenzelm discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
Fri, 08 Jul 2011 15:17:40 +0200 wenzelm standardized String.concat towards implode;
less more (0) -3 tip