debug_printf("-Release %d\n", pool_malloc);
else
debug_printf("-Release %6p %-20s %4d %d\n", (void *)bb, filename,
linenumber, pool_malloc);
debug_printf("-Release %d\n", pool_malloc);
else
debug_printf("-Release %6p %-20s %4d %d\n", (void *)bb, filename,
linenumber, pool_malloc);