#866 Run batch tool file format

[Jeremy Faden]

The run batch tool was somewhat thrown together back in the day, and it turns out to be very useful. It's file format for saving batch files is clumbsy, being a newline-delimited list of arguments. When there are 65000 files to process, this results in a completely unreadable file.

I'm tweaking the .batch file format so that the parameter arguments are a JSONArray of strings, but there may be other things we want to change. This is to document.

So here is an example of the new format:

{
    "param1": "nc",
    "param1Values": [
        "1",
        "2",
        "3",
        "4",
        "5"
    ],
    "param2": "size",
    "param2Values": [
        "100",
        "400"
    ],
    "script": "https://github.com/autoplot/dev/blob/master/demos/2019/20190726/demoParams.jy?nc=4&noise=0.4&size=400&interference='F'&sc='Z1'
&font='xkcd Script'"
}

[Jeremy Faden]

setenv newBatchFileFormat=true will use the new format with 20260124a and newer.

[Jeremy Faden]

See https://github.com/autoplot/dev/blob/master/demos/2019/20190726/runBatchNew.batch for an example.