> From: "Gisle Vanem"
> Date: Sun, 2 Mar 2014 17:28:41 +0100
>
> If it's the value of 'batch_mode_shell' we speak of, it can easily be
> changed by the new "load" feature. This diff:
>
> --- Git-Latest/makeint.h 2014-02-09 15:03:22 +
> +++ makeint.h 2014-03-02 17:10:53 +
> @@ -593,
"Paul Smith" wrote:
HOWEVER. I don't know nearly enough about all the variations and
different possibilities on Windows to make sound judgements on the
specific situation, so if Eli is OK with it then I'm OK with it.
If it's the value of 'batch_mode_shell' we speak of, it can easily be
chang
