fix: make command line consistent (part 1)

[lovettchris]

Note: in order to ensure I do not break the vscode-lean4 extension I will do this in 2 stages. First is to add only new options then I can move vscode extension over to those then later to remove the old options (-NoMenu and -PromptOnError).

Chris Lovett: From your discussion in https://github.com/leanprover/vscode-lean4/pull/151 let me summarize:

• add powershell -NoModifyPath to map to the no-modify-path elan-init option (hmmm, the vscode extension probably should be using this option).
• remove -PromptOnError since elan-init doesn't have that option (and do this part in vscode extension).
• change -NoPrompt to -NoMenu to match the -no-prompt option in elan-init.

Sebastian Ullrich: Okay, that sounds acceptable. Whether the extension should modify the path is a good question. I think people will expect leanto work from their cmdline as well after installation.

[lovettchris]

Thanks, the matching vscode-lean4 PR is here: https://github.com/leanprover/vscode-lean4/pull/158