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;
less more (0) -1 tip