+/* Writes SIZE bytes from BUFFER into FILE,
+ starting at the file's current position,
+ and advances the current position.
+ Returns the number of bytes actually written,
+ which may be less than SIZE if end of file is reached.
+ (Normally we'd grow the file in that case, but file growth is
+ not yet implemented.) */