Wed, 10 Nov 2010 17:53:41 +0100 | wenzelm | use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading); | changeset | files |
Wed, 10 Nov 2010 16:05:15 +0100 | wenzelm | merged | changeset | files |
Wed, 10 Nov 2010 09:03:07 +0100 | blanchet | make SML/NJ happy | changeset | files |