mv fails with an access permission error. Script is not aborted.

[VladimirMarko]

While running the script on Windows 10, the following line fails: mv msys64 msys

Error message:

mv : Access to the path 'C:\Users\vladi\get-idris\msys64' is denied.
At C:\Users\vladi\get-idris\get-idris.ps1:112 char:9
+         mv msys64 msys
+         ~~~~~~~~~~~~~~
    + CategoryInfo          : WriteError: (C:\Users\vladi\get-idris\msys64:DirectoryInfo) [Move-Item], IOException
    + FullyQualifiedErrorId : MoveDirectoryItemIOError,Microsoft.PowerShell.Commands.MoveItemCommand

This is treated as a non-fatal error by the script, which merrily run on, but of course the installation fails.

Workaround: Open the get-idris.ps1 in PowerShell ISE and set a breakpoint (F9) on on the relevant line (112). Run the script (F5). When you hit the breakpoint, just continue the running the script (F5). The delay of user input ensures that vm can get the permission.