/* This is a very short C++ file with no license header. *
 * Because it's so short (3 lines), it is accepted (it
 * wouldn't be copyrightable anyway) */