Define PINOCCHIO_PRAGMA_DEPRECATED_HEADER

Define Documentation

PINOCCHIO_PRAGMA_DEPRECATED_HEADER(old_header, new_header)