Tom Tromey writes: > Ok to commit? Well, there was a discussion pointing out that much more would be needed, and it's probably not going to happen immediately. Your patch is still an improvement, so ahead and check it in. Thank you for handling this PR. ./A