I wrote,

> printf("%s",XXX) is semantically equivalent to puts(XXX) for all XXX
> for which the former is well-defined,

which is actually not true (blush!).  It's equivalent to
fputs(XXX,stdout).  If XXX can be proven to end in a newline, then it's
equivalent to puts(XXX') where XXX' is XXX minus that trailing newline.

/~\ The ASCII				der Mouse
\ / Ribbon Campaign
 X  Against HTML	       mouse@rodents.montreal.qc.ca
/ \ Email!	     7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B