/* -----------------------------------------------------------------------------
Dumping stuff in the stats file, or via the debug message interface
/* -----------------------------------------------------------------------------
Dumping stuff in the stats file, or via the debug message interface