slashes to backslashes #ifdef WIN32.  This is to cope with the fact
that Windows seems exceedingly unfriendly to slashes in shell commands,
as per recent discussion.