Sorry, the Windows batch file doesn’t work at the moment: VS code error
Edit: I abandoned the batch file. I can get the job done with a bash script: much nicer to program. And it can be operated with the same double-click as a batch.
Sorry, the Windows batch file doesn’t work at the moment: VS code error
Edit: I abandoned the batch file. I can get the job done with a bash script: much nicer to program. And it can be operated with the same double-click as a batch.