build on linux: set the repository where files are saved #4232
+29
−25
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Brief summary of changes
add of the option
-rto the build and install script to set the path of this repository (default into $HOME) so the home directory is remained "cleaned" if the user wants it to.Is is done only for Linux at this point. I could also add the modification of the MacOS one, but I wouldn't be able to test it. For Windows, I have no idea how it works ;)
Testing I've completed
On Linux, I could run the build and install script (without the tests, that fails, cf #4171)
Looking for feedback on...
The same process should be done for the mac os, and maybe windows ?
CHANGELOG.md (choose one)
I don't know, tell me 😉
This change is