Re: [code] ctrl-c frequently doesn't work on Windows.

From: Robert Gieseke <>
Date: Tue, 24 Oct 2017 18:00:45 +0200

Am 24/10/17 um 17:12 schrieb Mitchell:
>> Mitchell, what do you think, should the patch/workaround for the Windows
>> 10/GUI issue be included? If not it should at least go in the FAQ ...
> I'm curious if anyone else is experiencing this issue on Windows 10. (I don't have a Win10 machine to test this on.) Regardless, I'd prefer a more reasonable patch like the one I suggested in a previous reply, and not a patch that tries spawning processes and invoking batch files.

Sure - I wasn't suggesting to include an external dependency ... your
variant looks quite clean!


You are subscribed to
To change subscription settings, send an e-mail to
To unsubscribe, send an e-mail to
Received on Tue 24 Oct 2017 - 12:00:45 EDT

This archive was generated by hypermail 2.2.0 : Wed 25 Oct 2017 - 06:34:46 EDT