Subject: Re: bug#13661: 24.3.50; shell-command fails with w32-downcase-file-names

From: Stefan Monnier <[email-masked]>
Date: Sat, 09 Feb 2013 14:02:07 -0500

> Damn that w32-downcase-file-names option!

If we don't want people to use it, then let's mark it obsolete.

        Stefan