Boehm, Hans writes: > It's attached, but probably not very informative; __java_double is > understood by the front end. Oh, sorry, I forgot about that. Hmm. I'll have a look. Andrew.