// This is only here to make the API headers happy.