+rem The weird place we put the redirection is to make sure no extra\r
+rem whitespace winds up at the end of the Make variables, since some\r
+rem variables, e.g. INSTALL_DIR, cannot stand that. Yes, echo will\r
+rem write the blanks between the end of command arguments and the\r
+rem redirection symbol to the file. OTOH, we cannot put the\r
+rem redirection immediately after the last character of the command,\r
+rem because environment variable expansion can yield a digit there,\r
+rem which will then be misinterpreted as the file descriptor to\r
+rem redirect...\r