Am 26.05.2010 um 18:54 schrieb Makarius: > * Some tuning of the Poly/ML runtime to shorted the (busy) wait interval > for external processes from 100ms to 10ms. This improves reactivity > of the ML bash/bash_output functions, at the cost of burning a few > extra cycles.
That is excellent news! Thanks for doing this. Jasmin _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
