You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have a ~/.ghci that sets my prompt, and it doesn't get loaded when I run stack --docker ghci
I realize that my entire filesystem doesn't get mounted into the docker image, and that there are good isolation benefits for not mounting my entire home directory -- however, perhaps the ghci file could be copied in as a special case?
The text was updated successfully, but these errors were encountered:
Actually, a change in the last version was to add $HOME and $TMPDIR to the container - #1949
The issue is probably that it is not located in the container user's home folder (the stack user). So, we'd need to add some logic to stack ghci which knows to pass in a -ghci-script= argument with the user's .ghci.
Should be a mostly straightforward change, PRs appreciated :D
The main tricky bit is plumbing the info that we're in a docker container and where the home folder is. Perhaps the info is already available in the Reader.
I have a ~/.ghci that sets my prompt, and it doesn't get loaded when I run
stack --docker ghci
I realize that my entire filesystem doesn't get mounted into the docker image, and that there are good isolation benefits for not mounting my entire home directory -- however, perhaps the ghci file could be copied in as a special case?
The text was updated successfully, but these errors were encountered: