/* An empty file.  */