void flush_profile(int p)
Flushes the profile p from all ProfileCache objects obtained with get_profile_cache .