// Dummy header used in documentation build