>>>>> "Pedro" == Pedro Alves <pedro@codesourcery.com> writes: Pedro> How about we just delete catch_exception? It doesn't seem to add Pedro> any value. Works for me. I'm testing a patch. Tom